Efficient Proof Checking with LRAT in CADICAL (Work in Progress)

Abstract:
The proof format DRAT used in the SAT competition is rather inefficient to check, often even slower to check than it takes the SAT solver to solve the instance and generate the proof. Therefore we implemented witin the SAT solver CADICAL the possibility to generate LRAT proofs directly, where LRAT on the one hand is much easier and way more efficient to check, but on the other hand much harder to generate. Unlike previous approaches our implementation generates LRAT directly in the solver without intermediate translations. We further propose the tool LRAT-TRIM, which can trim redundant proof steps from LRAT proofs, which not only reduces proof size but also leads to much faster proof checking.