Open Source Ecosystems

MiniCARD 1.2, based on MiniSAT 2.2.0 Mark Liffiton and Jordyn Maglalang [email protected],[email protected]

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)