Theory and Practice of SAT and Combinatorial Solving

What served as the point of departure of this workshop is one of the most significant problems in all of mathematics and computer science, namely that of proving logic formulas. This is a problem of immense importance both theoretically and practically. On the one hand, it is believed to be intractable in general, and deciding whether this is so is one of the famous million dollar Clay Millennium Problems (the P vs. NP problem). On the other hand, today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas (such as hardware and software verification, electronic design automation, artificial intelligence research, cryptography, bioinformatics, and operations research, just to name a few examples).

During the last two decades there have been dramatic – and surprising – developments in SAT solving technology that have improved real-world performance by many orders of magnitude. However, while modern solvers can often handle formulas with millions of variables, there are also tiny formulas with just a few hundred variables that cause even the very best solvers to stumble. The fundamental question of when SAT solvers perform well or badly, and what underlying properties of the formulas influence performance, remains very poorly understood. Other practical SAT solving issues, such as how to optimize memory management and how to exploit parallelization on modern multicore architectures, are even less well studied and understood from a theoretical point of view.

Perhaps even more surprisingly, the best SAT solvers today are still based on relatively simple methods from the early 1960s (though the introduction of so-called conflict-driven learning in the 1990s was a very important addition), searching for proofs in the so-called resolution proof system. Although other mathematical methods of reasoning are known that are much stronger than resolution in theory, in particular methods based on algebra (Gröbner bases) and geometry (cutting planes), attempts to harness the power of such methods have mostly failed to deliver significant improvements in practical performance for SAT solving. And while resolution is a fairly well-understood proof system, even very basic questions about these stronger algebraic and geometric methods remain wide open.

This is an interesting contrast to developments in neighbouring areas such as, e.g., constraint programming and mixed integer programming. There much more powerful methods of reasoning are successfully used to guide the search, but compared to SAT solving the attempts to employ conflict-driven learning have had much less of an impact. Also, while for SAT solvers it is at least possible to understand some aspects of their performance (by analysing proof systems such as resolution), a corresponding theoretical framework for constraint programming and mixed integer linear programming seems to be mostly missing.

In this workshop, we gathered leading researchers working on SAT and other challenging combinatorial optimization problems in order to stimulate an increased exchange of ideas between theoreticians and practitioners. As discussed above, previous editions of this workshop series at the Banff International Research Station, Schloss Dagstuhl, Fields Institute, and Casa Matemática Oaxaca have had a major impact on the involved communities and has helped to create bridges and stimulate the emergence of a joint research agenda. We are happy to report that the October 2022 workshop at Schloss Dagstuhl fully delivered on the expectation of serving as the valuable next step on this journey. During recent years we have already seen how computational complexity theory can shed light on the power and limitations on current and possible future techniques for SAT and other optimization problems, and and that problems encountered on the applied side can spawn interesting new areas in theoretical research. We see great potential for continued interdisciplinary research at the border between theory and practice in this area, and believe that more vigorous interaction between practitioners and theoreticians could have major long-term impact in both academia and industry.

A strong case can be made for the importance of increased exchange between the two fields of SAT solving on the one hand and proof complexity (and more broadly computational complexity) on the other. Given how many questions that would seem to be of mutual interest, it is striking that the level of interaction had been so low until our workshop series started with the first two meetings in Banff in 2014 and Dagstuhl in 2015. Below, we outline some of the concrete questions that served as motivation for organizing our second Dagstuhl workshop in this series in 2022, and for broadening the scope from Boolean satisfiability to combinatorial solving and optimization in general. We want to stress that this inst is far from exhaustive, and we believe that one important outcome of the seminar was to uncover also other questions at the intersection of theoretical and applied research, and of different research areas within combinatorial solving and optimization.

The scientific program of the seminar consisted of 29 presentations. Among these there were 14 50-minute surveys of different core topics of the workshop. These talks occupied most of the morning schedule Monday-Thursday, and were intended to make sure that the diverse audience would have a bit of a common background for the more technical talks reporting on recent research projects. The list of survey talks and speakers were as follows:

• $\mathrm{■}$

  SAT: interactions between theory and practice (Olaf Beyersdorff)

• $\mathrm{■}$

  SAT and computational complexity theory (Ryan Williams)

• $\mathrm{■}$

  Proof complexity and SAT solving (Jakob Nordström)

• $\mathrm{■}$

  Efficient proof search in proof complexity, a.k.a. automatability (Susanna de Rezende)

• $\mathrm{■}$

  Satisfiability modulo theories (SMT) solving (Nikolaj Bjørner)

• $\mathrm{■}$

  Quantified Boolean formula (QBF) solving and proof complexity (Meena Mahajan)

• $\mathrm{■}$

  Constraint programming (Ciaran McCreesh)

• $\mathrm{■}$

  Mixed integer linear programming (Ambros Gleixner)

• $\mathrm{■}$

  Algebraic methods for circuit verification (Daniela Kaufmann)

• $\mathrm{■}$

  First-order theorem proving (Laura Kovacs and Martin Suda)

• $\mathrm{■}$

  Automated planning (Malte Helmert)

• $\mathrm{■}$

  Formally verified combinatorial solvers (Mathias Fleury)

• $\mathrm{■}$

  Certifying solvers with proof logging (Armin Biere)

• $\mathrm{■}$

  Formally verified proof checking for certifying solvers (Yong Kiam Tan)

The rest of the talks were 25-minute presentations on recent research of the participants. The time after lunch each day was left for self-organized collaborations and discussions, and there was no schedule on Wednesday afternoon.

Based on polling of participants before the seminar week, it was decided to have an open problem session on Thursday afternoon. The poll also asked whether a panel discussion should be organized, but the support for this idea was weaker, and several participants emphasized that the workshop program should not be too dense and that the evenings should be left free of any program. Therefore, the organizers decided not to have a panel discussion. As a nice contribution, some of the participants of the workshop organized a music night on the last evening of the workshop.

The study of clause redundancy in Boolean satisfiability (SAT) has proven significant in various terms, from fundamental insights into preprocessing and inprocessing to the development of practical proof checkers and new types of strong proof systems. I will present our recent work on liftings of the recently-proposed notion of propagation redundancy — based on a semantic implication relationship between formulas — in the context of maximum satisfiability (MaxSAT), where of interest are reasoning techniques that preserve optimal cost (in contrast to preserving satisfiability in the realm of SAT). We establish the strongest MaxSAT-lifting of propagation redundancy allows for changing in a controlled way the set of minimal correction sets in MaxSAT. This ability is key in succinctly expressing MaxSAT reasoning techniques and allows for obtaining correctness proofs in a uniform way for MaxSAT reasoning techniques very generally. I will also highlight some interesting directions for future work.

This talk provides a brief survey on the relations between proof complexity and SAT solving. What can proof complexity tell us about the strength and limitations of SAT solving? Why should practitioners be interested in proof complexity results and why should theorists study SAT solving? What have we achieved in the past 25 years and which problems remain open?

Many critical applications crucially rely on the correctness of SAT solvers. Particularly in the context of formal verification, the claim by a SAT solver that a formula is unsatisfiable corresponds to a safety or security property to hold, and thus needs to be trusted. In order to increase the level of trust an exciting development in this century was to let SAT solvers produce certificates, i.e., by tracing proofs of unsatisfiability, which can independently be checked. In the last ten years this direction of research gained substantial momentum, e.g., solvers in the main track of the SAT competition are required to produce such certificates and industrial applications of SAT solvers require that feature too. In this talk we review this quarter of century of research in certifying the result of SAT solvers, discuss briefly alternatives, including testing approaches and verifying the SAT solver directly, mention exciting research on new proof systems produced in this context as well as how these ideas extend beyond formulas in conjunctive normal form.

The talk provides an overview of selected current trends in SMT solving theories and techniques https://z3prover.github.io/slides/proofs.html. An active area of discussion in the SMT community is around proof formats for SMT solvers. I give an introduction to current approaches pursued in solvers such as Z3, CVC5, VeriT and SMTInterpol.

In this talk, we take a deep-dive in the fascinating world of symmetry handling for Boolean Satisfiability, by reviewing three main classes of techniques: static symmetry breaking, dynamic symmetry breaking, and (dynamic) symmetric learning. We focus on proof logging techniques that have been developed for these symmetry handling methods, and in particularly study our recent symmetry handling methods built on VeriPB. We end with some open problems and challenges.

This talk will cover the relations between QBF resolution and QCDCL solving algorithms. Modelling QCDCL as proof systems we show that QCDCL and Q-Resolution are incomparable. We also introduce new versions of QCDCL that turn out to be stronger than the classic models. This talk is based on a couple of recent papers (joint with Olaf Beyersdorff and Tomas Peitl, which appeared in ITCS’21, SAT’21, SAT’22 and IJCAI’22).

The proof search problem is a central question in automated theorem proving and SAT solving. Clearly, if a propositional tautology $F$ does not have a short (polynomial size) proof in a proof system $P$, any algorithm that searches for $P$-proofs of $F$ will necessarily take super-polynomial time. But can proofs of “easy” formulas, i.e., those that have polynomial size proofs, be found in polynomial time? This question motivates the study of automatability of proof systems. In this talk, we give an overview of known non-automatability results, focusing on the more recent ones, and present some of the main ideas used to obtain them.

Solving combinatorial problems often combines SAT solving with different reasoning techniques. An external propagator can interpret the partial assignment built by the SAT solver during search and, based on such different reasoning methods, can construct clauses that are propagating or conflicting under that assignment. The use of such external propagators allows to directly guide the search of the SAT solver into a preferred direction, which can make problem solving in several problem domains more efficient (consider e.g. dynamic symmetry breaking). However, both the efficient combination of external propagators with the complex features of modern SAT solvers (e.g. proof logging and inprocessing), and the theoretical understanding of such combined reasoning methods are open problems. This talk, based on current work in progress, presents some of the design decisions that must be considered when external propagation is combined with modern CDCL solvers. We describe some challenges and formulate both practical and theoretical open questions about how to implement external propagation in CDCL in the presence of current SAT solver features such as proof logging, clause database reduction and inprocessing.

Comparing options between solvers is a complicated task. There are three main ways: runtime options (with the risk of not understanding requirements between features), compile-time option (with the issue of testing and making the code very complicated), or different versions of the source code. A second question is how to measure the performance without implementing the most advanced version. This (short) talk should serve as a basis for discussion on how to organize the development of a solver with various options.

In this talk, I present the two main approaches to verify solvers: partial verification (usually bottom-up from code to the specification) and complete verification (usually top-own from the specification towards the code). The former approach present many imilarities to verify checkers, whereas the latter starts with a full formalization of underlying lgorithm. I compare the approaches and show where the main challenges are.

Today’s state-of-the-art solvers for the general class of mixed integer programs exhibit both exact and heuristic properties. Both aspects are crucial for their lasting relevance in academic and industrial practice. In this talk, we give an overview of methods implemented and successfully used in mixed-integer programming solvers and try to point out connections to satisfiability solving and pseudo-Boolean optimization. We conclude by outlining our efforts to address the ubiquitous use of floating-point arithmetic in virtually all fast mixed integer programming solvers and report advances in performant roundoff-error-free MIP solving with proof logging [1].