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.