[ download | compile | create ]
Cube and Conquer software
This page provides access to software used in our 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.
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