MiniCard: An efficient cardinality solver based on MiniSAT
C++ Shell Other
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
core
encodings
minicard
minicard_encodings
minicard_simp_encodings
mtl
tests
utils
.gitignore
LICENSE
README

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.


HISTORY
-------

Version 1.2 added duplicate-literal handline 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