From Crossing-Free Resolution to Max-SAT Resolution

Mohamed Sami Cherif (1) , Djamal Habet (1) , Matthieu Py (1)

1 COALA - COntraintes, ALgorithmes et Applications

Adapting a SAT resolution proof into a Max-SAT resolution proof without considerably increasing its size is an open problem. Read-once resolution, where each clause is used at most once in the proof, represents the only fragment of resolution for which an adaptation using exclusively Max-SAT resolution is known and trivial. Proofs containing non read-once clauses are difficult to adapt because the Max-SAT resolution rule replaces the premises by the conclusions. This paper contributes to this open problem by defining, for the first time since the introduction of Max-SAT resolution, a new fragment of resolution whose proofs can be adapted to Max-SAT resolution proofs without substantially increasing their size. In this fragment, called crossing-free resolution, non read-once clauses are used independently to infer new information thus enabling to bring along each non read-once clause while unfolding the proof until a substitute is required.

Mots clés: 2012 ACM Subject Classification Theory of computation → Proof theory phrases Satisfiability; Satisfiability; Proofs; Max-SAT resolution

Domaines: Intelligence artificielle [cs.AI]

Mohamed Sami Cherif, Djamal Habet, Matthieu Py. From Crossing-Free Resolution to Max-SAT Resolution. 28th International Conference on Principles and Practice of Constraint Programming (CP 2022), Jul 2022, Haifa, Israel. ⟨10.4230/LIPIcs.CP.2022.12⟩. ⟨hal-03979371⟩