Below follows descriptions for all the instances in ECGRID-FromCNF, EC_ODD_GRIDS, EC-RANDOM-GRAPHS-FromCNF, EC_RANDOM_GRAPHS, and SUMINEQ.
## EVEN COLOURING (EC) FORMULAS ##
These are the Eulerian cycle even colouring (EC) formulas described by Markstrom in http://jsat.ewi.tudelft.nl/content/volume2/JSAT2_11_Markstrom.pdf , except that the
output format used here is not CNF/DIMACS but the pseudo-Boolean format specified in the document http://www.cril.univ-artois.fr/PB12/format.pdf .
All of these instances are unsatisfiable
ECGRID-FromCNF and EC_ODD_GRIDS: These formulas are easy for pseudo-Boolean reasoning (i.e., cutting planes) as well as for CDCL reasoning (i.e., resolution)
in theory.
For EC-RANDOM-GRAPHS-FromCNF and EC_RANDOM_GRAPHS: These formulas are easy for pseudo-Boolean reasoning (i.e., cutting planes) but are hard for CDCL reasoning
(i.e., resolution).
## 3-COLOURING FORMULAS ##
These formulas encode graph 3-colouring instances. The graphs are
chosen with a very particular structure, however, so that the
generated formula instances are easy for pseudo-Boolean reasoning
(i.e., the cutting planes proof system) but not for CDCL (i.e., the
resolution proof system).
All of these instances are unsatisfiable
## SUM INEQUALITY FORMULAS ##
These formulas are generated from directed acyclic graphs (DAGs) with
fan-in 2 and a unique sink. With every vertex we associate d distinct
variables, where d is an 'arity' parameter chosen at formula generation.
For a given arity d, which should be at least 2, let d' = d if d is
odd and d' = d - 1 otherwise (so that d' is always odd). Then the
sum inequality formula consists of the following inequalities:
(1) For every source vertex v a SOURCE AXIOM
2 \sum_{i=1}^{d} v_i >= d'
(2) For every non-source w with predecessors u and v a SUM AXIOM:
2 \sum_{i=1}^{d} w_i >= \sum_{i=1}^{d} (u_i + v_i)
(3) For the unique sink z the SINK AXIOM:
2 \sum_{i=1}^{d} v_i <= d'
These formulas are clearly unsatisfiable, since for every source at
least half of the variables is true by (1) ; this propagates upwards
in the DAG thanks to (2); but for the sink node less than half of
the variables should be true by (3).
These formulas are easy for pseudo-Boolean reasoning (i.e., cutting planes) as well as for CDCL reasoning (i.e., resolution) in theory.
## plain and extracted files ##
The *.plain.pb files are clauses only.
This CNFs have been parsed with the tool CuPaCD, which is able to
detect cardinality constraints syntactically and semantically from
CNFs, as described in
Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey:
Detecting Cardinality Constraints in CNF. SAT 2014: 285-301.
For this task, the default setup has been used.
The restuling formulas are stored in the *.extracted.pb files.