seeSAT     -     visualize solutions to random SAT problems

Free teaching software by David MacKay

seeSAT

As the number of clauses in a random 3-SAT problem on M variables is increased, the set of solutions decreases in size, starting out as a single interconnected cluster, then falling into a number of unconnected clusters once a threshold is passed (in the vicinity of 4M clauses).

This perl program visualizes a part of this phenomenon with pretty animations, for small SAT problems. Only a part, because the 'falling into a number of unconnected clusters' phenomenon can only be seen reliably when M is about 1000. This program is recommended for M about 10 only.

Installing

Download perl program. Make directories called g and o.
Optionally download .gnuplot and Xdefaults.gnu in order to inherit my preferred linestyles and linecolors. If you have not defined any linestyles, you'll need my .gnuplot; append it to your ~/.gnuplot. If you want my colour scheme, execute xrdb < Xdefaults.gnu.

Running

The program is used thus

unix>       solns.p M=10

When you run the program, it creates a sequence of random 3-SAT problems (of which more later), writes out a load of files in g/ and o/, and spits out a list of possible gnuplot commands. For example, the output might look like this

1024

Starting
load 'g/g10.1'
....
load 'g/g10.40' 
load 'g/g10.41' 
load 'g/g10.42' 
load 'g/g10.43' 
load 'g/g10.44' 
time 45, no solutions left
# gnuplot   
 load 'g/g10' 

Viewing

If you want to see the whole sequence of solutions as clauses are added in one at a time, without animation, use the final two instructions, i.e., start gnuplot then load the file

unix>  gnuplot
== GNUPLOT welcome message ==
gnuplot>  load 'g/g10' 
Now hit return and you will see a sequence of say 45 pictures showing
the set of points in the hypercube that satisfy the first clause;
the set of points in the hypercube that satisfy clauses 1-2;
the set of points in the hypercube that satisfy clauses 1-3;
the set of points in the hypercube that satisfy clauses 1-4;
...
the set of points in the hypercube that satisfy clauses 1-45; The hypercube is projected down randomly onto two dimensions.

The solution points are shown with point style 5 (cyan in the above example). Points that violate one clause are shown in another point style (4, green). Points that violate 2 or 3 clauses are shown as dots in style 3 or 2. Edges between solution points are shown (magenta). Edges between solution points and points that violate one clause are shown (red). I have this .gnuplot file in my home directory, and I use these X defaults.

After you have tapped through this sequence you might like to jump in at some point and see the hypercube animated. If you type

load 'g/g10.12' 
then you will see an animation starting from step 12. The animation takes a fixed 4-dimensional projection of the hypercube, and projects it into 2 dimensions in a sinusoidally varying manner. You may perceive the resulting image as an elastic 3-dimensional grid that is being sheared and rotated. There are two wobbles per time step.

Things to notice

Lines with the same slope correspond to flips of a particular variable. If there are lots of magenta lines with the same slope, that means a particular variable is free to flip in many solution states.

Variations

If you set M to a value greater than 16, be prepared for large files to be generated, and for the plots to take a long time to generate.

If you want to dive straight in to an animation, first type this:

gnuplot>   setmeto1 = 1
then load the corresponding file.

License

This software is released under the GNU General Public License.

Bibliography


David MacKay
Last modified: Sun Jul 6 00:35:22 2003