sat-analysis
A version of MiniSat capable of producing very verbose traces and some simple analysis tools.
There are presently two main directories
-
minisat/contains the modified version of MiniSat 2.2.0 and associated tools. Note that this was based off of the version from http://minisat.se/downloads/minisat-2.2.0.tar.gz on the MiniSat website, which is approximately what competed in Sat-RACE 2010. Some more changes have been made to the version hosted on GitHub at https://github.com/niklasso/minisat -
bench/contains some very simple DIMACS-format CNF instances for testing
Getting started
MiniSat with trace generation
First compile MiniSat just as you would the normal version of MiniSat
cd minisat
export MROOT=$(pwd)
cd core # It doesn't with the preprocessing wrapper yet
make rs
This produces a statically linked executable named minisat_static
with aggressive compiler optimization, assertions turned off, and
no debug symbols. You may prefer to use the build target d instead of rs
if you would prefer a less optimized executable including assertions
suitable for use with gdb. The resulting executable will be named
minisat_debug.
Note: Some recent versions of g++ with support for C++11 are throwing
some warnings. I haven't bothered making the necessary changes to
silence these warnings as I occasionally examined the diff between
the version of MiniSat in this repo and the original MiniSat 2.2.0 source,
in order to check that I haven't introduced changes to solver behavior.
I have prefered to keep this diff relatively clean.
As of right now, conflict clause minimization is still off by default as described in the report, but I believe there is no good reason for this and if somebody were to run more experiments, you might as well change the default value back to deep minimization.
Now you can run MiniSat on CNF instances and get trace files. For example:
./minisat_static ../../bench/simple/easy-sat.cnf easy-sat.trace
./minisat_static ../../bench/simple/three.cnf three.trace
easy-sat.cnf is satisfiable, while three.cnf is unsatisfiable. The resulting .trace file format is described in the report appendix.
You may be interested to try:
./minisat_static --help
If running MiniSat on a more challenging instance, the trace will be very large! Do not place the output file in a location corresponding to a NFS or otherwise synchronized over a network, as then MiniSat's performance will likely be limited by the available network bandwidth. Even worse, if you are running MiniSat on a server you are remotely connected to, MiniSat might eat up all the available network bandwidth and make connecting to the server or performing any further operations difficult until it has finished running the instance and writing out the trace file!
Analysis tool
The tool for parsing and analyzing the trace files generated by MiniSat are in
the minisat/analysis/ subdirectory.
In that subdirectory,
analyze_trace.cc is the main file of interest.
The build system borrows from the MiniSat build system, so to compile this file
simply execute make rs or make d to generate the executable named analyze_static or analyze_debug, respectively.
The resulting executable very simply takes the input trace file as its first argument and the output file as a second argument. The output file will contain a single line with numbers separated by commas. It is intended that these output files can be concatenated to produce a single CSV file with data from the analysis of many instances. The columns are the trace filepath, number of events, critical events, skippable events, branches, critical branches, skippable branches, implications, critical implications, and skippable implications.
You can also use the build target run-simple to generate all the trace files
associated with running MiniSat on all the benchmarks in bench/simple/,
and use the build target analyze-simple to analyze all those traces and
produce corresponding CSV files.
That is, inside the minisat/analysis/ subdirectory, run the commands:
make run-simple
make analyze-simple