File test_v3_r8_vr5_c1_s8257.smt2-stp212.lrat
is an incorrect LRAT file (downloaded from Peter Schneider-Kamp's page) and generated from this old version of drat-trim
. Hence, the following command is expected to fail.
../bin/satans-cert test_v3_r8_vr5_c1_s8257.smt2-stp212.cnf -l test_v3_r8_vr5_c1_s8257.smt2-stp212.lrat
This bug of drat-trim
has been fixed. So, the following command should succeed (provided that drat-trim
is up-to-date in the environment) to produce a certified 'UNSAT !' answer.
../bin/satans-cert test_v3_r8_vr5_c1_s8257.smt2-stp212.cnf -drat-file test_v3_r8_vr5_c1_s8257.smt2-stp212.drat
Occasionally, some SAT-solvers give incorrect answers in SAT competition (and thus get disqualified). For example, from the parallel track of SAT competition 2017, it appears that solver abcdsat_p answers 'UNSATISFIABLE' on the 'mp1-9_38.cnf' file of the benchmark. Here, no DRAT proof is given, because it was only required in the main track. But, this 'mp1-9_38.cnf' is proved 'SAT !' by using CaDiCaL+satans-cert.