kp-minicard: A C++ repository from karpiu

KP-MiniCARD 1.0 based on MiniCARD 1.1
 Michal Karpinski and Marek Piotrow
 <karp@cs.uni.wroc.pl>,<mpi@cs.uni.wroc.pl>
--------

This is the extended version of the MiniCARD v. 1.1 by Mark Liffiton and Jordyn Maglalang.
We have added the implementation of two new encodings based of selection networks:

  4-Wise Selection Network
  4-Odd-Even Selection Network

We have also provided our implementation of the Pairwise Cardinality Networks.
Those three encodings can be found in `encodings/Encodings_MW.h`.

Content of the original MiniCARD 1.1 README file follows:

MiniCARD 1.1, 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.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
karpiu/kp-minicard
