Determinism in the Certification of UNSAT Proofs
Tomer Libal (Inria, Paris), Xaviera Steele (American University of, Paris)

TL;DR
This paper explores a highly trusted, simplified certifier for UNSAT proofs that, with format restrictions, can certify arbitrarily large proofs without extensive search, enhancing trustworthiness in SAT solver verification.
Contribution
It introduces a simplified certifier approach that, under certain format restrictions, can certify large proofs efficiently and reliably.
Findings
Format restrictions can eliminate the need for search.
The certifier can handle proofs of arbitrary size.
High trust level due to simplicity of certifier.
Abstract
The search for increased trustworthiness of SAT solvers is very active and uses various methods. Some of these methods obtain a proof from the provers then check it, normally by replicating the search based on the proof's information. Because the certification process involves another nontrivial proof search, the trust we can place in it is decreased. Some attempts to amend this use certifiers which have been verified by proofs assistants such as Isabelle/HOL and Coq. Our approach is different because it is based on an extremely simplified certifier. This certifier enjoys a very high level of trust but is very inefficient. In this paper, we experiment with this approach and conclude that by placing some restrictions on the formats, one can mostly eliminate the need for search and in principle, can certify proofs of arbitrary size.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
