I am making the source code to a satisfiability program available, and
if there's enough interest, I will post it in comp.lang.lisp (1500
lines of code). Mail to ········@sail.stanford.edu.
The program is competitive with the fastest complete algorithms that I
know of. If you use a propositional inference engine in your work, give
this one a try. If you haven't put a significant amount of time an
effort into your inference system, this program is probably faster in a
majority of cases.
On Mitchell, Selman, Levesque hard spot problems, the program takes
from 1 minute to 15 minutes on 150 variable instances, including
unsatisfiable instances, averaging under 10 minutes. The program
appears to run in time N*2^(N/22) on MSL hard spot instances.
Easy Instances: Using the program, the author (me) discovered
empirically that almost all randomly generated 4-regular graphs (and
indeed, almost all randomly generated k-regular graphs, with
sufficiently many vertices), are 3-colorable. Instances with
thousands of vertices were translated to 3-sat and then colored.
There is a fairly simple counting argument that proves this empiricaal
result. Empirically, the 3-coloring problem on almost all (in
Bollobas sense) 4-regular graphs is easy (near linear time).
However, the main potential practical result is that, given a random
instance of an NP-complete problem, and then translating it to 3-sat,
does not necessarily make the resulting instance hard. The program
appears to run in near O(N) time on almost all of these 3-coloring
instances. Please note, however, these so-called "easy" instances appear
to be quite hard for the Davis-Putnam algorithm.
Fairly Hard Instances: There is a simple method to generate instances
that are significantly harder than the MSL hard spot. Generate random
3-clauses such that each variable appears 5 times positively and 5
times negatively. The resulting 3-cnf formulae tend to be harder and
smaller than MSL hard spot formulae, but also tend to be almost always
satisfiable, given more than 100 or so variables. The program tends
to run in time 2^(N/17) or so on these instances, but they could get
even harder as N gets larger. These "5-5-regular" instances are the
hardest, almost always satisfiable, 3-CNF problems that I know of.
Hardest Known Instances: The hardest (based on size of 3-CNF formulae)
of any instances are 6-5-regular (each variable occurs 6 times
positively and 5 times negatively), with many of these being
unsatisfiable. 150 variable instances of these problems can take
several hours.
I'm very interested in "in practice" kinds of instances. I wonder how
hard the NP-complete instances that actually arise in areas outside of
CS theory really are.
If you'd like to trade "hard" instances, let me know.
I may not be on the net after Christmas, because the job hunting
situation in this area is very bad. So if you'd like the source code
for the program, let me know soon. Also, if you have any pointers to
"research programming" type jobs, I'd very much appreciate them.
Dan Pehoushek