From: Tortolo
Subject: Davis Putman Algorithm
Date: 
Message-ID: <26176b48.0110180543.6a845c68@posting.google.com>
Under what circumstances does the Davis Putman algorithm produce
frequent failures high in the search tree?

Thanks,


Tortolo
From: Tim Bradshaw
Subject: Re: Davis Putman Algorithm
Date: 
Message-ID: <ey3y9m9f40o.fsf@cley.com>
* jcardena  wrote:
> Under what circumstances does the Davis Putman algorithm produce
> frequent failures high in the search tree?

Usually, when it's implemented in a language which does not check
array bounds.  Because it's a bit complicated, you tend to get lots
of off-by-one errors in indexing with resulting obscure failures and
core dumps (Unix) or reboots (Windows).  These failures often occur
quite high in the search tree, although some particularly insidious
failures can be misdiagnosed as premature successes.  This often
happens if you use the wrong kind of name-mangling or build gcc
without thread support.

--tim