Abstract
Oliver Kullmann
Title: Representing problems to SAT solvers: basic theory, basic questions
Abstract: The starting point is a "problem" to be solved by a SAT solver. How can we "represent" it for "good" solving complexity, that's the question. In my talk I will outline the basic approaches, both theoretical and practical ones.
Ciaran McCreesh
Title: Encodings and Consistency from a Constraint Programming Perspective
Abstract: Constraint programmers like to make use of exotic concepts like variables that have more than two possible values, and global constraints like "all different". There are two ways of handling these richer variables and constraints: though propagation algorithms, or through encoding to a simpler format such as SAT. Getting a good propagation algorithm or encoding is extremely important in practice. We don't have a precise theoretical understanding of what "good" means here, although an important starting point is consistency. I'll explain what different kinds of consistency (arc, generalised arc / domain, bounds, ...) mean for propagators, and how these concepts can and can't be mirrored by encodings to SAT with unit propagation. Finally, I'll touch very briefly on some connections to recent work on proof logging.
Maria Bonet
Title: Advantages and limitations of Dual-Rail MaxSAT
Abstract: Joint work with: Sam Buss, Alexey Ignatiev, Joao Marques-Silva and Antonio Morgado.
Conflict-driven clause learning (CDCL) is at the core of the success of modern SAT solvers. In terms of propositional proof complexity, solvers with CDCL and restarts have been shown as strong as general Resolution.
Improvements to SAT solvers can be realized either by improving existing algorithms, or by exploiting proof systems stronger than CDCL.
Recent work proposed an approach for solving SAT by reduction to Dual-Rail MaxSAT. The proposed reduction coupled with MaxSAT resolution represents a new proof system, DRMaxSAT, which was shown to enable polynomial time refutations of pigeonhole formulas, in contrast with either CDCL or general resolution.
We have investigated the DRMaxSAT proof system, and shown that DRMaxSAT p-simulates general resolution, that $\AC^0$-Frege$+\PHP$ p-simulates DRMaxSAT, and that DRMaxSAT can not p-simulate the Cutting Planes proof system.
We can also use the dual-rail MaxSAT encoding with any of the algorithms that solve MaxSAT, like the core-guided algorithms, or the minimum hitting set algorithms, to solve some hard unsatisfiable instances. We show theoretically and experimentally good performance of this algorithms on families of formulas like pigeon-hole principle, the double pigeon-hole principle, and parity (only for the minimum hitting set algorithm).