Re: * * * Best SAT algorithm? * * *

From: Wcncom (wcncom_at_aol.com)
Date: 12/26/03 

Date: 26 Dec 2003 03:14:38 GMT

In article <bm774m$3gt$1@ls219.htnet.hr>, "dalix" <dalibor.hrg@fer.hr> writes:

>Hello.
>I have three questions!
>
>What is the best known algorithm ( O(?) ) for decision of SAT
>predicate??????
>Does the quantum algorithm for SAT problem exists?
>Are there only probabilistic algorithms for solving that problem or maybe
>there is something like resolution rule method (it's used to show that 2-SAT
>is in P)??
>

Take a look at
http://www.satlive.org
http://www.satlib.org
for lots of info on latest developments in SAT.
Modern SAT solvers can solve 3-SAT in something
like O(2^(N/20)) empirical run time. There is a SAT competition
held every year, with results posted on satlive.org,
and winning solvers can be downloaded
from the above websites.

Last I heard, the best solver for random 3-SAT instances
is "kcnfs", which you can find at these sites. It can refute
or find solution to 400 variable instances in a few minutes;
for a 600 variable instance it takes 12 hours.
The winner of the overall contest was "siege".
"siege" can solve many industry examples of 100,000
variables and more in minutes, although it craps out
for randomized instances over 300 variables.

There are many randomized "walkers" which solve SAT
by a randomized hill-climb. For example, look for the
word "unitwalk" in www.google.com
You will find a very good hill-climbing solver.

Quantcast