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 program to decide the satisfiability of circuits expressed in 3-variable conjunctive normal form, and an accompanying arbitrary precision integer library. I coded it purely as an exercise, to keep my coding, analytical, and problem solving faculties sharp. First published online in 2008, 3SAT has been in development since 2003, begun shortly after completing my doctoral studies.

What is 3sat-1.0.1.tar.gz and how do I use it?

3sat-1.0.1.tar.gz is a tar-ed, gzip-ed archive, containing the source files for building the 3SAT problem generator and solver, including a simpler arbitrary-precision integer arithmetic library (to facilitate problems with more than 64 input variables). 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

Alternatively, type:

$ ./3sat 96 1024

at the command-line, where 96 is the number of variables, and 1024 is the number of clauses in the problem instance, and 3sat will generate a random 3SAT problem with 1024 three-variable clauses chosen from among 96 variables. If keeping the randomly-generated problem is desired, simply enter "-o filename" at the end of the aforementioned command-line; this file can later be used in conjunction with the "-i" option described above.

The 3SAT solver is now multithreaded! The 3SAT solver can now partition the search space among some number of threads, which will attack 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 the other still-running 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, e.g.:

$ ./3sat -i expr1 -t 2

The default (which happens without an explicit "-t" parameter) is to use a single thread. (Anyone have access to a 32-node server of quad-core Itanium 9300 CPUs this can be tried on? Anyone?)

As the solver executes, it will silently test input variable configurations. To obtain the status of the solver's progress, you can send a SIGUSR1 signal to the solver process. From a separate window, get the process ID of the solver:

$ ps aux | grep 3sat
 6085  p2  R+     6:25.22 ./3sat 96 1024

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 variable inputs 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 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³ · 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³² bit patterns.

Tell me about the arbitrary-precision integer library.

I wanted the arbitrary integer precision library to be very light-weight, and built it from scratch as an exercise. (Gotta stay sharp!) 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 add, subtract, AND, OR, XOR, invert, compare (i.e., greater than [or equal], less than [or equal], or equal), and shift integer_t objects. 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.

Tell me about 3SAT's algorithm.

While having matured significantly since version 0.0.2, the algorithm is actually not terribly complex at all. Starting with the all-zeros bit pattern, the solver tests each pattern 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 the bit pattern, then moves on to test the next bit pattern. Since there are exponentially many bit patterns, the solver tries where it can to skip 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 clauses caused the 0 evaluation, and to increment the bit pattern counter by some amount greater than one. Consider, if you will, that each circuit in a 3SAT problem consists of a set of clauses AND'd together:

C₁ · C₂ · C₃ · ... · 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₁ 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 evaluation to 1. In the latter case, let the 0-evaluating clause be (v₈₃ + v₄₇ + v₂₉), and recall that there are 96 variables in the circuit: v₁ through v₉₆. Further, let the present evaluation bit pattern be represented by binary integer B. If the present evaluation bit pattern yields 0, then so will all 2²⁸ other possible configurations of v₁ through v₂₈, featuring variables v₈₃, v₄₇, and v₂₉ set as they are in B. And since the solver processes the bit patterns in ascending order, it is safe to "skip" the evaluation of these bit patterns.

In other words, think of B as composed 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 concatentating them to yield the new B. The circuit evaluation loop may now be rejoined, starting from clause C₁, having saved ourselves as many as 2²⁸ needless evaluations.

An additional savings is realized by sorting the clauses in descending order, after the random circuit generation, and prior to the ascending order bit pattern evaluation loop. Also, 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 bit pattern 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 one 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 satisfiability function executes, it masks out the relevant bits for C_j from B, and checks to see if they match the aforementioned 0-evaluating values. 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 cuts running time by about 62% relative to 0.9.1 for expr1 on my Intel Celeron.

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 (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 absolutel 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. On my Celeron, using input circuit expr1, this optimization yielded an 89% reduction in running time.

What are the known glitches in 3SAT?

Finally, one day, as an interesting challenge, it might be fun to port my solver to CUDA.

How do I contact the author?

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 integer library. Wha'd'ya think?

Notes and final comments...

In addition to the sample problem file, expr1, 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 -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 -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 its hash, 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.

Legalese...

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 Problem Generator and Solver. Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013; John Haskins, Jr.