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.
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.
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'
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 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.
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.
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 = 1then load the corresponding file.
This software is released under the GNU General Public License.