This is the code for the Minisat+SP SAT solver which implements Symmetry 
Propagation (SP). A paper describing the algorithm has been accepted at 
ICTAI 2012, and will be published in due time. An older (and hence 
uncopyrighted) version of the paper is available at this repository under the 
name "Symmetry Propagation: Improved DynamicSymmetry Breaking in SAT.pdf".

For full benchmark results, see the folder "full benchmark results".

For cnf test files, see the folder "cnf test files".

To compile and run Minisat+SP, go to the last paragraph of this readme.

To download this repository without using git, click on the "ZIP" button in the
upper left corner of the web page "https://github.com/JoD/minisat-SPFS".

================================================================================
Quick Install

- Decide where to install the files . The simplest approach is to use
  GNU standard locations and just set a "prefix" for the root install
  directory (reffered to as $PREFIX below). More control can be
  achieved by overriding other of the GNU standard install locations
  (includedir, bindir, etc). Configuring with just a prefix:

  > make config prefix=$PREFIX

- Compiling and installing:

  > make install

================================================================================
Configuration

- Multiple configuration steps can be joined into one call to "make
  config" by appending multiple variable assignments on the same line.

- The configuration is stored in the file "config.mk". Look here if
  you want to know what the current configuration looks like.

- To reset from defaults simply remove the "config.mk" file or call
  "make distclean".

- Recompilation can be done without the configuration step.

  [ TODO: describe configartion possibilities for compile flags / modes ]

================================================================================
Building

  [ TODO: describe seperate build modes ]

================================================================================
Install

  [ TODO: ? ]

================================================================================
Directory Overview:

minisat/mtl/            Mini Template Library
minisat/utils/          Generic helper code (I/O, Parsing, CPU-time, etc)
minisat/core/           A core version of the solver
minisat/simp/           An extended solver with simplification capabilities
doc/                    Documentation
README
LICENSE

================================================================================
Examples:

Run minisat with same heuristics as version 2.0:

> minisat <cnf-file> -no-luby -rinc=1.5 -phase-saving=0 -rnd-freq=0.02

================================================================================
Minisat with Symmetry Propagation (SP):

After running the Quick Install (see above), simply compile Minisat the normal
way. For the tests, we used the following command:

> make cr

which compiles the Minisat release version without the simplification extension.

Next, run minisat with a given cnf-file:

> ./minisat_core <cnf-file>

The SP-code will automatically check whether a file with the name 
<cnf-file>.txt is available at the same location as <cnf-file>. If this is the 
case, it will extract symmetries from this file, which should be in the format 
as generated by Shatter (http://www.aloul.net/Tools/shatter).