Download your copy of 3SAT, the 3SAT problem generator and solver 3sat-1.0.1.tar.gz, by, John Haskins, Jr. today! |
3SAT Solver is a toolset for deciding the satisfiability of circuits expressed in 3-variable conjunctive normal form, consisting of: (1) the satisfiability solver software; and (2) an large-integer math library used by the solver. I coded it purely as an exercise, to keep my coding, analytical, and problem solving faculties sharp. First published online in 2008, 3SAT Solver has been in development since 2003, begun shortly after I completed my doctoral studies.
3sat-1.0.1.tar.gz is a tar'd, gzip'd archive, containing the source files for building 3SAT Solver and the large-integer arithmetic library. The source files should easily compile and run on many different flavors of UNIX and UNIX-like systems (e.g., Linux, FreeBSD, NetBSD, MacOS X, OpenBSD, BSDI, NeXT, BeOS, IRIX, OSF/1, Mach, Solaris, SunOS, AIX, HP/UX). The compilation procedure described in the Makefiles has been tested with GNU's versions of the C compiler on Fedora, Ubuntu, Solaris, and MacOS X.
To unpack the archive, gunzip and un-tar as in the example below:
$ gunzip -c 3sat-1.0.1.tar.gz | tar -xf -
All files should be deployed into a directory named 3sat-1.0.1. To build the executables,
$ cd 3sat-1.0.1 $ make
[NOTE: This software requires GNU make, version 3.81 or better.] Voila! 3SAT is ready to go, but first it will be necessary to tell the shell where to find the included arbitrary-precision integer library. Assuming Bash on Linux:
$ export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$PWD/jhjr_math
Assuming Bash on MacOS X:
$ export DYLD_LIBRARY_PATH=$LD_LIBRARY_PATH:$PWD/jhjr_math
Now, you're all set to run:
$ ./3sat -i expr1.cnfIn the above example the "-i" parameter instructs the 3sat binary to pull the 3SAT problem instance from the file expr1.cnf (which is included in the 3sat-1.0.1.tar.gz archive). Once the problem is loaded, 3sat will immediately begin searching for a solution to determine the problem's satisfiability.
Alternatively, the solver is also capable of constructing a randomly-generated problem instace; to wit:
$ ./3sat 96 1024
Here, "96" is the number of variables, and "1024" is the number of clauses in the problem instance. Hence, the 3sat binary will generate a random 3SAT problem with 1024 three-variable clauses chosen from among 96 variables. If you would like to keeping the randomly-generated problem for future use, simply append "-o filename" at the end of the previous command-line; to wit:
$ ./3sat 96 1024 -o random_96_1024.cnf
3SAT Solver is also multithreaded! For some number of threads, the search space is partitioned, allowed each thread to attack its share of the problem in parallel. Additionally, if one thread completes its allotted slice of the search space while others are still running, the finished thread will query its still-running peer threads, and split the workload of the thread with the most processing left to do. To access this functionality, use the "-t" command-line parameter; to wit:
$ ./3sat -i expr1.cnf -t 2
The default (which happens without an explicit "-t" parameter) is to use a single thread. (Anyone have access to a large SMP server packed full of quad-core Itanium 9300 CPUs this can be tried on? Anyone?)
As the solver executes, it silently tests input variable configurations, only printing to stdout those input variable configurations that satisfy the circuit. In a long-running execution, it might be interesting to learn how far the solver has progressed; to query the solver's progress, you can send a SIGUSR1 signal to the solver process. For the sake of illustration, assume that the 3sat binary was executed: (1) in a windowed envinronment; and (2) as above, with randomly-generated circuit parameters 96 and 1024. From a new window, get the 3sat process ID:
$ ps aux | grep 3sat 6085 p2 R+ 6:25.22 ./3sat 96 1024 -o random_96_1024.cnf
Then, find out the signal number for SIGUSR1, and send the signal:
$ kill -l 1) SIGHUP 2) SIGINT 3) SIGQUIT 4) SIGILL 5) SIGTRAP 6) SIGABRT 7) SIGEMT 8) SIGFPE 9) SIGKILL 10) SIGBUS 11) SIGSEGV 12) SIGSYS 13) SIGPIPE 14) SIGALRM 15) SIGTERM 16) SIGURG 17) SIGSTOP 18) SIGTSTP 19) SIGCONT 20) SIGCHLD 21) SIGTTIN 22) SIGTTOU 23) SIGIO 24) SIGXCPU 25) SIGXFSZ 26) SIGVTALRM 27) SIGPROF 28) SIGWINCH 29) SIGINFO 30) SIGUSR1 31) SIGUSR2 $ kill -30 6085
In the window where the solver is running, you should see somethng like the following:
solve(): [STATUS REPORT] s = 000000000003990b2996000000000000
The string "000000000003990b2996000000000000" is a hexidecimal-formatted bitmap of the input variable configuration presently being tested by the solver. Since there are 96 bits' worth of variables to test, the solver must test bit patterns from 00000000000000000000000000000000 through 00000000ffffffffffffffffffffffff; hence, the solver has so far tested less than 1% of the possible input variable configurations. [NOTE: The "STATUS REPORT" messages are printed to stderr, separate from the circuit's solutions, which are printed to stdout.]
Naturally, the probability of finding a satisfying bit pattern increases as the number of clauses is reduced, e.g.:
$ ./3sat 32 128 main(): MAX(n_clause) = 39680 main(): getrusage() -> 26381 4270 main(): starting solve()... solve(): [SOLUTION] s = 0000000000000000000000001a0d9a0f solve(): [SOLUTION] s = 0000000000000000000000001e0d9a0f solve(): [SOLUTION] s = 00000000000000000000000080098c39 solve(): [SOLUTION] s = 00000000000000000000000080098c3b solve(): [SOLUTION] s = 00000000000000000000000081098c39 solve(): [SOLUTION] s = 00000000000000000000000081098c3b solve(): [SOLUTION] s = 0000000000000000000000008109cc39 solve(): [SOLUTION] s = 0000000000000000000000008109cc3b solve(): [SOLUTION] s = 00000000000000000000000084098c39 solve(): [SOLUTION] s = 00000000000000000000000084098c3b solve(): [SOLUTION] s = 00000000000000000000000085098c39 solve(): [SOLUTION] s = 00000000000000000000000085098c3b solve(): [SOLUTION] s = 0000000000000000000000008509cc39 solve(): [SOLUTION] s = 0000000000000000000000008509cc3b solve(): [SOLUTION] s = 000000000000000000000000850d8c30 solve(): [SOLUTION] s = 000000000000000000000000850d8c32 solve(): [SOLUTION] s = 000000000000000000000000850d8e30 solve(): [SOLUTION] s = 000000000000000000000000850d8e32 main(): getrusage() -> 20866332 48795
In this sample run, the program begins by telling the maximum number of non-repeating 3-variable clauses that can be formed from 32 variables: 2^{3} · binom(32,3) = 39,680. Then, it invokes the getrusage system call to obtain the amount of time (in microseconds) spent generating the circuit; the first number is the amount of time spent by the CPU on the process's behalf in user space, and the second number is the amount spent in the kernel. Finally, the solver does its work, reporting satisfying bit patterns as it encounters them, and reporting the amount of time spent processing the 2^{32} bit patterns.
I wanted the large-integer library to be very light-weight, and built it from scratch as an exercise. The library defines a type integer_t, which is a simple structure that gives the length (in bytes and bits) of the integer, and supplies a pointer to an array of unsigned char bytes that contain the number itself. To manipulate these, the library supplies a series of functions to operate on them: add, subtract, AND, OR, XOR, invert, compare (i.e., greater than [or equal], less than [or equal], or equal), and shift. Internally, the library uses rapid-access FILO stacks (one per thread) of integer_t objects to accelerate the arithmetic routines.
And, as you've probably already guessed, I named the library, and indeed all the routines with the jhjr_ prefix strictly for my own ego's sake: jhjr → JHJr → John Haskins Jr.
While having matured significantly since version 0.0.1, the algorithm is actually not terribly complex at all. Starting with the all-zeros bit pattern, the solver tests successive patterns against the circuit. If the circuit output evaluates to 0, the solver moves on to the next bit pattern; if the circuit output evaluates to 1, the solver reports it, then moves on to test the next bit pattern. Since there are exponentially many bit patterns, the solver skips those configurations that would obviously cause the circuit to evaluate to 0.
The question of obvious 0 evaluation is a matter of ongoing research, but the approach used in this solver is to decide which of the circuit's clauses caused the 0 evaluation, and to increment the bit pattern counter by some amount greater than one. Consider that each circuit in a 3SAT problem consists of a set of clauses AND'd together:
C_{1} · C_{2} · C_{3} · ... · C_{m}
where each clause consists of a set of 3 variables OR'd together:
C_{j} = (v_{c} + v_{b} + v_{a})
Each variable may be optionally inverted, changing the sense of its value during the clause's evaluation.
The solver evaluates the circuit by traversing the list of clauses in order, from C_{1} to C_{m}. If a clause evaluates to 1, the solver proceeds to the next clause, since there is still a chance that the entire circuit will evaluate to 1; if a clause evaluates to 0, the solver does not proceed to the next clause, since there is no chance that the entire circuit will evaluate to 1. In the latter case, let the 0-evaluated clause be (v_{83} + v_{47} + v_{29}), and assume that the solver is operating on a circuit with 96 input variables: v_{1} through v_{96}. Let the present evaluation bit pattern be represented by binary integer B, formed by concatenating the binary values of all 96 input variables, i.e., B = v_{96}v_{95}...v_{1}. If B yields 0, then so will all 2^{28} possible configurations of v_{1} through v_{28}, featuring variables v_{83}, v_{47}, and v_{29} set as they are in B. And since the solver processes bit patterns in ascending order, it is safe to "skip" the evaluation of these bit patterns.
In other words, think of B as the concatenation of bit patterns B_{96..29} and B_{28..1}. "Skipping" unnecessary evaluations is achieved by incrementing B_{96..29} by one, setting all the bits of B_{28..1} to zero, and re-concatentating them to yield the new B. The circuit evaluation loop may now be resumed, starting over from clause C_{1}, having saved as many as 2^{28} needless evaluations.
An additional savings is realized by sorting the clauses in descending order according to the "rank" of the variables contained in each clause; to wit: v_{2} > v_{1}.
Considerable savings were also realized by short-circuiting clause evaluations. Consider again, the clause template:
C_{j} = (v_{c} + v_{b} + v_{a})
If the variable v_{c} evaluates to 1, then---because the variables' outcomes are logically OR'd together---the entire clause C_{j} will evaluate to 1; hence it is unnecessary to spend any further time evaluating v_{b} and v_{a}. Similarly, if v_{b} evaluates to 1, then evaluation of v_{a} can be safely skipped. This short-circuit evaluation was added to version 0.7.4, and cut running time relative to version 0.7.3 by about 45%.
While efficient, the integer library functions are still very slow relative to native integer arithmetic. Hence, reducing the number of arithmetic operations necessary to evaluate each B yielded large running time savings. Previously, for each C_{j}, the bits corresponding to inputs v_{a}, v_{b}, and v_{c} were individually masked out from B, and tested; if any of the three evaluated to 1, the whole clause evaluated to 1, and B was tested against C_{j+1}. In 0.9.2, before the satisfiability function is invoked, each C_{j} is checked to determine the single bit pattern among v_{a}, v_{b}, and v_{c} that will cause the whole clause to evaluate to 0; this value is stored in a table. (It is important to note that only one configuration of a clause's three input variables will cause the clause to evaluate to 0.) As the solver executes, it masks out from B, the relevant bits for C_{j}, and checks to see if they match the aforementioned 0-evaluating values table. If they do not match, then the clause must evaluate to 1, and the function continues with C_{j+1}. In this way, version 0.9.2 cut running time by about 62% relative to 0.9.1 for expr1.cnf.
Another significant performance boost, which was introduced in version 0.9.3, came from allowing threads that had completed their slice of the search space to split the workload of sibling threads that still had work to do. (Why leave a processing element idle?) On a quad-core Xeon, processing expr3.cnf (which, by the way, has no satisfying configurations), this course-grained thread-level load balancing yielded a roughly 27% reduction in running time relative to version 0.9.2. Also introduced in 0.9.3, the lowest of the low-hanging fruit for efficiency was to make the width of the integer_t objects only as wide as absolutely necessary. In version 0.9.2, this width was controlled by the macro NVAR_MAX in 3sat.c, and was set to 512 bits. In version 0.9.3, NVAR_MAX became a variable, set according to the number of input variables to the circuit. This optimization yielded an 89% reduction in running time for expr1.cnf.
The source must be built with GNU make version 3.81 or better. (Version 3.80 will not work!)
I have a half-baked idea for obtaining partial input variable solutions given the (possibly untrue) assumption that the circuit is satifiable under some unknown configuration of the inputs. If m of n variables can be solved, then the search space collapses from 2^{n} possible input configurations to only 2^{n - m}... which is still exponential, but "less" so.
February 2015
I recently found a paper, "Solving the 3-Satisfiability Problem Using CUDA Architecture," (written in Polish) at Studia Informatica, which cites this very Web page. If the online translation engine that I used is to be believed, the authors, Widuch and Krawczyk, rendered my above-described algorithm in CUDA. Awesome!
January 2015
Just noticed a bug report from Daniel Milstein that the code does not seed the random number generator. That bug will be fixed in the next release. Thanks, Daniel!
August 2014
I have begun refactoring the code to make it more modular.
I can be contacted via e-mail at predator@cs.virginia.edu, but I cannot guarantee a timely response.
I would be very interested in feedback from users of the solver, and/or the large-integer library.
In addition to the sample problem file, expr1.cnf, the archive also contains a file with all the satisfying solutions to that problem: expr1.solutions. The latter was collected with the following command-line:
$ ./3sat -i expr1.cnf -t 4 | grep SOLUTION | sort > expr1.solutions
I have found it useful to compare the results from sundry tweaks to the solver engine by hashing the results output by 3sat, and comparing that to the hash of expr1.solutions, e.g.:
$ ./3sat -i expr1.cnf -t 4 | grep SOLUTION | sort | md5sum - expr1.solutions 5426f0343ccd79bc91b4939f3a0ab731 - 5426f0343ccd79bc91b4939f3a0ab731 expr1.solutions
Since I trust the results in expr1.solutions, and the hash produced by 3sat matches, I know that the solutions generated by 3sat are correct. (The sort step is necessary because in a multithreaded process, there is no telling the order in which solution(s) will be found; including sort on single-threaded invocations harms nothing.)
Also: I know that there are dozens more sophisticated methods for solving 3SAT problem instances. This whole project was mostly an exercise for myself to keep my programming, analytical, and problem solving skills sharp. Put another way: There are plenty of ways to improve this program; why not give it a try... and send me a pointer to the result.
The 3SAT solver is free software, released under a BSD license. Neither I nor the University of Virginia guarantee the suitability of this software for any purpose, that the executables or any other part of the distribution be stable, correct or bug-free. This software is offered in the hope that others will find it useful and elucidating. Use at your own risk.
Latest version: 25 February 2013
3SAT Solver. Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015; John Haskins, Jr. |