Benchmark for Cardinality Constraint modeling.

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. As of Dec. 3 2012, the files in this page have changed (the benchmarks have been regenerated and a description file has been added). The old version can be accessed here.

Feedback on this page is more than welcome:
email address

Documents

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.

How to use the documents

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:

What you need to know

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/:

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.

What you don't need to know (how the benchmark was generated)

In progress. Please send me an email if this section has not been filled in six months.

Bibliography


Ban
Last modified: 3 Dec 2012