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