Overview

This is a set of examples of how to use the MiniSat API. While sparsely populated at the moment this is intended to serve as a sort of FAQ for general encoding questions, as well as MiniSat-specific usage issues.

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

• Install MiniSat. Below the location of MiniSat headers and library files is referred to as $MINC and $MLIB respectively. If installed in a system-wide default location these locations are not necessary to specify by the user, and the configuration step becomes simpler.

• Each example is built separately. Change directory to the example of your interest and follow the steps below.

• Configure the library dependencies:

  [ the exact details here may be simplified in the future ]

  make config MINISAT_INCLUDE=-I$MINC make config MINISAT_LIB="-L$MLIB -lminisat"

• 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

Examples

• Minumerate:

  This simple example gives solutions to two frequently recurring encoding patterns: enumerating models and finding minimal models. The default mode of the program is to read a CNF in DIMACS format and either enumerate all models, or only minimal models.

  In this example models are merely counted, but it should be fairly clear how to do further processing. Further, minimal models are defined with respect to the number of true variables. In applications it would be more useful to be able to define minimality with respect to a set of literals to allow minimizing a subset of variables and take polarity into account.