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


march_cc compile using: make
iLingeling compile using ./configure; make (first in druplig, then in lingeling directory)


Experiments on symmetry-breaking proofs (Section 7.1)
Experiments with iLingeling (Section 7.2)