Open problems in interference and proofs for SAT solving

Description

Enormous progress has been made over the last decade in proofs for SAT solving. The combination of satisfiability-preserving inferences, deletion instructions and clausal proofs allowed the development of effective and compact proof formats, such as DRAT. Further advancements include extended inference power, featured in DPR and (W)SR proofs, as well as hinted proofs that can be checked with verified tools, like LRAT and FRAT. This fast evolution has left some problems unsolved, and some paths unexplored. In this talk I will argue that these gaps in our understanding and development of proofs for SAT are relevant for certification, and for SAT solving itself. In my talk I will focus on (at most, depending on time restrictions) four of these problems. First, the proliferation of proof systems has created a cornucopia of different checkers and formats with slightly different properties, capabilities and even semantics. Some approaches are to every extent superior, yet their implementation is still spotty; some approaches have been accepted at face value without considering drawbacks or alternatives. We will review some design decisions in proof systems that may be worth revisiting. Second, deletion instructions, which first appeared in DRUP as a performance-related feature, have quietly become more relevant, and more problematic. CDCL-based SAT proofs are dominated by one specific flavor of deletion, which I call linear deletion. However, this is not the case in adjacent fields. Both VeriPB and WSR depart from this idea, and in doing so they enable new paths in proofs and in reasoning.

Period	16 Oct 2024
Event title	Dagstuhl Seminar 24421: SAT and interactions
Event type	Conference
Location	GermanyShow on map