Download your copy of 3SAT, the 3SAT problem generator and solver 3sat-1.0.1.tar.gz, by, John Haskins, Jr. today!


What is 3SAT Solver and where did it come from?

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.

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

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:

All files should be deployed into a directory named 3sat-1.0.1. To build the executables,

[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:

Assuming Bash on MacOS X:

Now, you're all set to run:

In 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:

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 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:

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:

Then, find out the signal number for SIGUSR1, and send the signal:

In the window where the solver is running, you should see somethng like the following:

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.:

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: 23 · 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 232 bit patterns.

Tell me about the large-integer library, jhjr_math.

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.

Tell me about 3SAT Solver algorithm.

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:

C1 · C2 · C3 · ... · Cm

where each clause consists of a set of 3 variables OR'd together:

Cj = (vc + vb + va)

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 C1 to Cm. 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 (v83 + v47 + v29), and assume that the solver is operating on a circuit with 96 input variables: v1 through v96. 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 = v96v95...v1. If B yields 0, then so will all 228 possible configurations of v1 through v28, featuring variables v83, v47, and v29 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 B96..29 and B28..1. "Skipping" unnecessary evaluations is achieved by incrementing B96..29 by one, setting all the bits of B28..1 to zero, and re-concatentating them to yield the new B. The circuit evaluation loop may now be resumed, starting over from clause C1, having saved as many as 228 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: v2 > v1.

Considerable savings were also realized by short-circuiting clause evaluations. Consider again, the clause template:

Cj = (vc + vb + va)

If the variable vc evaluates to 1, then---because the variables' outcomes are logically OR'd together---the entire clause Cj will evaluate to 1; hence it is unnecessary to spend any further time evaluating vb and va. Similarly, if vb evaluates to 1, then evaluation of va 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 Cj, the bits corresponding to inputs va, vb, and vc 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 Cj+1. In 0.9.2, before the satisfiability function is invoked, each Cj is checked to determine the single bit pattern among va, vb, and vc 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 Cj, 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 Cj+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.

What are the known glitches in 3SAT?

The source must be built with GNU make version 3.81 or better. (Version 3.80 will not work!)

What are the author's plans for the future of 3SAT?

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 2n possible input configurations to only 2n - m... which is still exponential, but "less" so.

News

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.

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 large-integer library.

Notes and final comments...

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:

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.:

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.

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