What a Difference a Variable Makes
For review purposes only
This page will provide access to proofs and tools presented in our TACAS 2018 paper.
Table 1:
CNF formulas
PR proofs
existing proofs
plain proofs
optimized proofs
Table 2:
CNF formulas
PR proofs
DRAT proofs
CLRAT proofs
Proof checking tools:
PR2DRAT. Compile as follows: gcc pr2drat.c -O2 -o pr2drat
DRAT-trim. Compile as follows: gcc drat-trim.c -O2 -o drat-trim