MIAO/BARC talk by Paul Beame

Tuesday, April 21, 2026, Paul Beame, Professor at the University of Washington, USA, will be giving a joint MIAO/BARC talk on "Extending CDCL to disjunctions of parity equations". 

We will run this as a hybrid seminar, so if you are not able to participate on site, it is also possible to join virtually at https://lu-se.zoom.us/j/61925271827.

Abstract:
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. 

Bio:
Paul received his B.Sc. in Mathematics in 1981, an M.Sc. in Computer Science in 1982, and Ph.D. in Computer Science in 1987, all from the University of Toronto. He was a Post-doctoral Research Associate at M.I.T. for the 1986-87 academic year and joined the University of Washington in 1987. Paul’s research is in pure and applied computational complexity. A major focus of his research is in proving lower bounds on the resources needed for solving computational problems. Such topics include communication complexity, time-space tradeoff lower bounds, circuit complexity, proof complexity, and data structures. Another focus of his research is on problems related to formal reasoning, including SAT-solving. His research includes applications of computational complexity in formal verification of software and hardware (currently focused on verifying non-linear arithmetic), in the study of databases, and in AI, particularly in knowledge representation, learning, and probabilistic inference.

Host:
Jakob Nordström