Extended Resolution Simulates DRAT
This page will provide access to proofs and tools presented in our SAT 2018 paper.
The ER proofs below are in the LRAT format, while the ones produced by EBDDRES are in the
tracecheck format.
hole20.cnf:
hole20.pr
hole20.drat
hole20.lrat
hole20-Cook.lrat
hole30.cnf:
hole30.pr
hole30.drat
hole30.lrat
hole30-Cook.lrat
hole40.cnf:
hole40.pr
hole40.drat
hole40.lrat
hole40-Cook.lrat
hole50.cnf:
hole50.pr
hole50.drat
hole50.lrat
hole50-Cook.lrat
tph8.cnf:
tph8.pr
tph8.drat
tph8.lrat
tph12.cnf:
tph12.pr
tph12.drat
tph12.lrat
tph16.cnf:
tph16.pr
tph16.drat
tph16.lrat (too large, available on request)
tph20.cnf:
tph20.pr
tph20.drat
tph20.lrat (too large, available on request)
Urquhart-s5-b1.cnf:
Urquhart-s5-b1.pr
Urquhart-s5-b1.drat
Urquhart-s5-b1.lrat
Urquhart-s5-b1.trace
Urquhart-s5-b2.cnf:
Urquhart-s5-b2.pr
Urquhart-s5-b2.drat
Urquhart-s5-b2.lrat
Urquhart-s5-b2.trace
Urquhart-s5-b3.cnf:
Urquhart-s5-b3.pr
Urquhart-s5-b3.drat
Urquhart-s5-b3.lrat
Urquhart-s5-b3.trace
Urquhart-s5-b4.cnf:
Urquhart-s5-b4.pr
Urquhart-s5-b4.drat
Urquhart-s5-b4.lrat
Urquhart-s5-b4.trace
Proof transformation tool:
Available on GitHub at https://github.com/benjaminkiesl/drat2er