Cube and Conquer software

This page provides access to software used in our HVC'11 paper.
It won the best-paper award of HVC'11.


lingeling-limami2-aa61f7a-110831.tar.gz ]

iCNF.tar.gz ]

march_cc.tar.gz ]

appli.7z ]

The iCNF files are the ones used for the second phase of cube-and-conquer in the HVC'11 paper. March_cc partitions an input CNF and outputs the learnt clauses and the cubes in /tmp/. Combined with the input CNF they from a iCNF file. The appli.7z archive contains the application benchmarks of the SAT 2009 competition.


To compile lingeling and iLingeling, unpack the archive and run configure and make.
To compile march_cc run make.

Creating and solving cubes

The following script (cubeconquer in the march_cc archive) can be used to solve CNF file FILE using the cube-and-conquer method decribed in the paper:

./lingeling FILE -s -o /tmp/simp.cnf
./march_cc /tmp/simp.cnf
echo "p inccnf" > /tmp/simp.icnf
cat /tmp/simp.cnf | grep -v c >> /tmp/simp.icnf
cat /tmp/learnt >> /tmp/simp.icnf
cat /tmp/cubes  >> /tmp/simp.icnf
./ilingeling /tmp/simp.icnf -v -b 12