Compositional Propositional Proofs
For Review Purposes Only
This page will provide access to tools and logs presented in our LPAR-20 paper.
Proof Checkers
DRAT-trim compile using: gcc drat-trim.c -O2 -o drat-trim
Drabt compile using: ./configure; make
Cube-and-conquer
march_cc compile using: make
iLingeling compile using ./configure; make (first in druplig, then in lingeling directory)
Logs
Experiments on symmetry-breaking proofs (Section 7.1)
Experiments with iLingeling (Section 7.2)