README

MiniCARD 1.2, based on MiniSAT 2.2.0
 Mark Liffiton and Jordyn Maglalang
 <mliffito@iwu.edu>,<jmaglala@iwu.edu>

MiniSAT originally by Niklas Eén and Niklas Sörensson

================================================================================

OVERVIEW
--------

MiniCARD is a *cardinality solver* based on MiniSAT [www.minisat.se].  MiniCARD
handles cardinality constraints natively, using the same efficient data
structures and techniques MiniSAT uses for clauses, giving it much better
performance on cardinality constraints than CNF encodings of those constraints
passed to a typical SAT solver.  It can read the standard DIMACS CNF format,
the OPB pseudo-boolean format (with linear cardinality constraints only), and
CNF+, a format that extends CNF to include cardinality constraints.  

The CNF+ format extends the DIMACS CNF format, adding the ability to specify
cardinality constraints alongside regular clauses like so:

  c Example: Two cardinality constraints followed by a clause
  p cnf+ 7 3
  1 -2 3 5 -7 <= 3
  4 5 6 -7 >= 2
  3 5 7 0

See the tests/in/ directory for example files.

Run minicard with the --help and --help-verb flags for details on command line
options.


REFERENCES
----------

A Cardinality Solver: More Expressive Constraints for Free (Poster Presentation)
  Mark H. Liffiton and Jordyn C. Maglalang
  in Proc. 15th International Conference on Theory and Applications of
     Satisfiability Testing (SAT-2012), 485-486, June 2012.

  Poster (with experimental data):
    https://sun.iwu.edu/~mliffito/publications/sat12_liffiton_minicard_poster.pdf

  Paper (2 page summary):
    https://sun.iwu.edu/~mliffito/publications/sat12_liffiton_minicard.pdf


HISTORY
-------

Version 1.2 added duplicate-literal handling in cardinality constraints.  Each
copy of a literal within a cardinality constraint will "count" separately
toward the constraint's bound.  For example, AtMost({x1, x1, x2}, 2) will be
violated if x1 and x2 are both True.  This allows for "instrumented" or
"implied" cardinality constraints.  For example, AtMost({y, y, x1, x2, x3}, 3)
is equivalent to y -> AtMost({x1, x2, x3}, 1).

Version 1.1 added a basic ability to parse and solve OPB-format instances
(http://www.cril.univ-artois.fr/PB12/format.pdf) in which the constraints are
limited to linear cardinality constraints only (i.e., all weights are -1 or
+1).  To solve OPB instances, use the -opb command line flag.


DIRECTORIES
-----------

[MiniCard directories]
  minicard/                 The core MiniCard solver with native AtMost constraints
  minicard_encodings/       A cardinality solver using CNF encodings for AtMosts
  minicard_simp_encodings/  The above solver with simplification / preprocessing
  tests/                    A set of simple test instances for the solvers
[original MiniSAT directories]
  core/                     The base MiniSAT solver
  mtl/                      Mini Template Library
  utils/                    Generic helper code (I/O, Parsing, CPU-time, etc)


BUILDING (release version: without assertions, statically linked, etc)
--------

  export MROOT=<minisat-dir>              (or setenv in cshell)
  cd { minicard | minicard_encodings | minicard_simp_encoding }
  gmake rs
  cp minicard_static <install-dir>/minicard