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.

Download

[ 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.

Compile

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