[Proof Complexity] MIAO seminar Tue Apr 21 at 14:00 CEST with Paul Beame: Extending CDCL to disjunctions of parity equations

[Jakob Nordström]

Dear all,

It is our pleasure to announce that next Tuesday April 21 at 14:00 CEST we will have the opportunity to listen to a seminar with Paul Beame from the University of Washington, who will give a talk titled "Extending CDCL to disjunctions of parity equations". You find the abstract at the bottom of this message.

We will run this as a MIAO hybrid seminar at the University of Copenhagen. Local participants are warmly welcome to the new location of the Algorithms and Complexity Section at Vibenshuset, Lyngbyvej 2, while other participants are equally warmly welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk<mailto:jn at di.ku.dk>.

Best regards,
Jakob Nordström

**********

Tuesday Apr 21 at 14:00 at the Algorithms and Complexity Section at the University of Copenhagen, Vibenshuset, Lyngbyvej 2, and on Zoom
Extending CDCL to disjunctions of parity equations
(Paul Beame, University of Washington)

Because conflict-driven clause learning (CDCL) SAT solvers produce proofs in the Resolution proof system, problems provably hard for Resolution are also provably hard for CDCL. Exponentially shorter proofs can sometimes be found using stronger proof systems such as Res(⊕), a generalization of Resolution to XNF formulas, whose constraints are disjunctions of parity equations ("linear clauses") such as (x ⊕ y) ∨ ¬(y ⊕ z). While some modern solvers like CryptoMiniSAT reason on Boolean clauses with separate parity equations, reasoning about more general linear clauses is less explored.

We present CDCL(⊕), a generalization of CDCL to XNF formulas, and prove a bidirectional connection with Res(⊕): CDCL(⊕) not only produces Res(⊕) proofs, but also polynomially simulates Res(⊕) given nondeterministic decisions and restarts, mirroring the classical relationship between CDCL and Resolution. Our key technical tool is a new set of inference rules for Res(⊕) that helps us translate Resolution-based subroutines such as 1-UIP clause learning. Altogether, CDCL(⊕)'s parity reasoning includes branching on arbitrary parity equations, linear-algebraic reasoning during unit propagation, and learning linear clauses through conflict analysis.

We provide a proof-of-concept implementation of CDCL(⊕) called Xorcle, which includes adaptations of existing CDCL heuristics to XNF formulas and an extension of LRUP proof logging that we call LRUP(⊕). On a selected suite of benchmarks focusing on native XNF formulas, Xorcle outperforms existing solvers such as Kissat and CryptoMiniSAT. Additionally, on Tseitin formulas written in CNF, even without preprocessing, Xorcle’s running time appears to scale nearly polynomially.

Joint work with Glenn Sun.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se




När du skickar e-post till Lunds universitet behandlar vi dina personuppgifter i enlighet med gällande lagstiftning. Mer om hur dina personuppgifter behandlas hittar du på Lunds universitets webbplats<https://www.lu.se/integritet>.


When you send emails to Lund University, we process your personal data in accordance with existing legislation. To find out more about the processing of your personal data, visit the Lund University website<https://www.lunduniversity.lu.se/about/contact-us/processing-of-personal-data-at-lund-university>.