This page presents a benchmark for modeling Cardinality Constraint properties in SAT. In my work on diagnosis of discrete-event systems by SAT, I happened to use cardinality constraint in conjunction with SAT problems, and therefore studied this type of constraints.
Feedback on this page is more than welcome:
The benchmark proposed here uses cardinality constraints on top of existing SAT problems derived from diagnosis of discrete-event system problems. The benchmark is partitionned in 10 archives.
Each cc.x.tar.gz
contains 60 archives, each
called cnf.z.y.x.tar.gz
(the
meaning of x
, y
, and
z
is explained below, but it is not
necessary to understand what they represent to use the
benchmark). Each subarchive generates a directory called
cnf.z.y.x/
and containing the
following files:
mobsfile
is the SAT problem in DIMACS format
(without the header).faultfile
contains the list of SAT variables in
mobsfile
on which the cardinality constraint is
defined.ccfile
is a cardinality constraint encoding in
DIMACS format proposed for this benchmark (description below);
the reason it is proposed is that we believe it is the most
efficient.ccfile.j
for all j in
{0,...,z} is a CNF (it should be a single unit clause) to
add to ccfile
in order to specify that the
cardinality constraint on the variables of
faultfile
is less or equal to j.
To test your implementation of cardinality constraint, you only
need to use mobsfile
and faultfile
.
The cardinality constraint should be defined on the variables of
faultfile
and concatenated with the CNF of
mobsfile
. The variables of mobsfile
should be defined such that there is no gap (if variables
v1 and v2 are used in mobsfile
, any
variable v3 such that v1 < v3 < v2 should be
used in mobsfile
as well); therefore, the
additional variables in your encoding should start after the
last variable of mobsfile
.
Following our SARA-09 paper (or our JFPC-08 paper, for a French
version), we advise you to use the variables in the order
proposed in faultfile
; another reasonnable order
would be: 1st, 21st, 41st, etc., 2nd, 22nd, 42nd, etc. 3rd,
23rd, etc. For more details about the relative impact of the
order, read the papers! (Please provide feedback if your
experiments contradict ours.)
The interesting (from the point-of-view of diagnosis and
possibly SAT) cardinality constraints for a problem
cnf.z.y.x/
lie for values
j in {0,...,z}. (The closer j to z,
the harder the problem -- except when the problem becomes
satisfiable.) The SAT problem mobsfile
is always
satisfiable, and so is the problem with cardinality constraint
j = z. It is usually the case that the problem is not
satisfiable for j < k. For some problem, in
particular if k is big, y = 'p' and j = k-1,
it might happen that the problem turns out to be satisfiable.
The differences between the problems are described next Section.
However it may be interesting to determine which SAT problems
are easy or hard to solve. In a problem
cnf.z.y.x/
:
mobsfile
problem is roughly linear in
z; second, the SAT problem including a cardinality
constraint becomes satisfiable for the value z (or very
close to this value).
As mentionned above, the benchmarks come with an implementation
of cardinality constraint. This implementation is based on
Bailleux and Boufkhad implementation (CP-03) with the UCG
ordering presented in our SARA-09 paper. The cardinality
constraint ≤ j is enforced by concatenating the
ccfile
and ccfile.j
to
mobsfile
. The fact that the same
ccfile
is used for any j might seem
inefficient for j < k; however, provided the encoding
is correct (why I believe is the case), the unit propagation on
the concatenation of ccfile
and
ccfile.j
should eliminate the variables and
clauses that wouldn't have been created if j = k.
In progress. Please send me an email if this section has not been filled in six months.