SAT and Interactions

Modern SAT solvers are often integrated as sub-reasoning engines into more complex tools to address problems beyond Boolean satisfiability. Consider, for example, solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration, and model counting. In our work, we have proposed a general interface for CDCL SAT solvers to capture the essential functionalities necessary to simplify and improve use cases that require more fine-grained interaction with the SAT solver than provided by the standard IPASIR interface.

In this talk I will briefly describe the interface and highlight the main changes made since its introduction. I will also present our ongoing work and the challenges and future work we are currently considering. The aim of the talk is to initiate further discussions with the other participants of the seminar to get a better understanding of the required features and typical use cases.

Algebraic statements involving matrices or linear operators appear in various branches of mathematics and related disciplines. In linear algebra and geometry, we study matrices and their properties as fundamental objects, while in functional analysis, linear operators help to analyse function spaces. Their applications range from the study of integral and differential equations to different tasks in the field of signal processing. In quantum mechanics, linear operators describe the evolution of quantum systems through the Schrödinger equation.

In this talk, we present a recently developed framework for proving first-order statements about identities of matrices or linear operators by performing algebraic computations. Our main result is a semi-decision procedure that allows to prove any true operator statement based on a single algebraic computation. We also discuss our software package operator_gb [2], which offers functionality for automating such computations, and we present the results of a recent case study [1].

The propositional model counting problem #SAT asks to compute the number of satisfying assignments for a given propositional formula. Recently, three #SAT proof systems kcps[1] (knowledge compilation proof system), MICE[2] (model counting induction by claim extension), and CPOG[3] (certified partitioned-operation graphs) have been introduced with the aim to model #SAT solving and enable proof logging for solvers. Prior to this paper, the relations between these proof systems have been unclear and very few proof complexity results are known. We completely determine the simulation order of the three systems, establishing that CPOG simulates both MICE and kcps, while MICE and kcps are exponentially incomparable. This implies that CPOG is strictly stronger than the other two systems.

The packing chromatic number of a graph is the minimum $n$ so that the graph may be vertex-coloured with $n$ colours so that vertices coloured never appear at distance $i$ or less from one another (thus colour 1 behaves as in a usual proper colouring). We survey results about the packing chromatic number of various infinite lattices and present bounds for the infinite square lattice that have been found by various methods, including SAT-solving, which were recently perfected to the answer 15.

We prove robust supercritical trade-off results for depth versus width in resolution and for the Weisfeiler-Leman algorithm, where optimizing one complexity measure even approximately causes worse than brute-force worst-case behaviour for the other measure. These are the first trade-offs in these settings that are truly supercritical measured not only in the number of variables but in the size of the input.

AVATAR is a powerful but poorly-understood component of the Vampire theorem prover, first introduced by Andrei Voronkov circa 2014 [1]. In essence, AVATAR allows a SAT solver to manage the propositional structure of splitting decisions during proof search. I introduce AVATAR, chart its development over the last ten years (such as practical experiments [2] and AVATAR modulo theories [3]), and give some future directions [4].

Enormous progress has been made over the last decade in proofs for SAT solving. The combination of satisfiability-preserving inferences, deletion instructions and clausal proofs allowed the development of effective and compact proof formats, such as DRAT. Further advancements include extended inference power, featured in DPR and (W)SR proofs, as well as hinted proofs that can be checked with verified tools, like LRAT and FRAT.

This fast evolution has left some problems unsolved, and some paths unexplored. In this talk I will argue that these gaps in our understanding and development of proofs for SAT are relevant for certification, and for SAT solving itself. In my talk I will focus on (at most, depending on time restrictions) four of these problems.

First, the proliferation of proof systems has created a cornucopia of different checkers and formats with slightly different properties, capabilities and even semantics. Some approaches are to every extent superior, yet their implementation is still spotty; some approaches have been accepted at face value without considering drawbacks or alternatives. We will review some design decisions in proof systems that may be worth revisiting.

Second, deletion instructions, which first appeared in DRUP as a performance-related feature, have quietly become more relevant, and more problematic. CDCL-based SAT proofs are dominated by one specific flavor of deletion, which I call linear deletion. However, this is not the case in adjacent fields. Both VeriPB and WSR depart from this idea, and in doing so they enable new paths in proofs and in reasoning.

Third, satisfiability-preserving inferences have recently come to be understood as reasoning without loss of generality. This enabled very powerful proof systems, but in practice these features are underutilized. In the last couple of years, however, the interest on these techniques has rekindled. I will review what is new, and what theoretical and practical problems still remain to be solved.

Finally, I will explain how well (or not) these advancements extend to other solving paradigms, including non-CNF SAT solving, (D)QBF and model checking, and what roadblocks exist that need further research.

PPSZ, for long time the fastest known algorithm for $k$-SAT, works by going through the variables of the input formula in random order; each variable is then set randomly to 0 or 1, unless the correct value can be inferred by an efficiently implementable rule (like small-width resolution; or being implied by a small set of clauses).

We show that PPSZ performs exponentially better than previously known, for all $k\ge 3$. We achieve this through an improved analysis and without any change to the algorithm itself. The core idea is to pretend that PPSZ does not process the variables in uniformly random order, but according to a carefully designed distribution. We write “pretend” since this can be done while running the original algorithm, which does use a uniformly random order.

I provide a short overview of modern first-order theorem proving, discussing the overall structure of a prover, including clausification and refutation core. For the latter part, we discuss saturation up to redundancy in the superposition setting. We also discuss implementation and search control.

Quantified Boolean Formulas (QBF) extend propositional formulas with quantifiers ranging over truth values. Satisfiability testing of QBFs is PSPACE-complete, and they can succinctly encode many problems arising in verification and synthesis. This talk provides an introduction to the main paradigms in QBF solving, Quantified CDCL and Expansion, and their corresponding proof systems. It also gives an overview of QBF proof complexity, highlighting the unique role of strategy extraction.

We initiate an in-depth proof-complexity analysis of polynomial calculus (Q-PC) for Quantified Boolean Formulas (QBF). In the course of this we establish a tight proof-size characterisation of Q-PC in terms of a suitable circuit model (polynomial decision lists). Using this correspondence we show a size-degree relation for Q-PC, similar in spirit, yet different from the classic size-degree formula for propositional PC by Impagliazzo, Pudlák and Sgall (1999). We use the circuit characterisation together with the size-degree relation to obtain various new lower bounds on proof size in Q-PC. This leads to incomparability results for Q-PC systems over different fields.

I will present how the search for finite models in first-order logic is typically translated into a sequence of SAT formulas, what kinds of symmetry breaking can be used to make these formulas easier to tackle and what extra challenges the multi-sorted setting brings.

SAT modulo Symmetries (SMS) is a framework for the exhaustive isomorph-free generation of combinatorial objects with a prescribed property. SMS relies on the tight integration of a CDCL SAT solver with a custom dynamic symmetry-breaking algorithm that iteratively refines an ordered partition of the generated object’s elements. This talk will discuss the basic concepts of SMS, some applications, and recent extensions to graph properties specified as general quantified Boolean formulas (QBF). In the second part of the talk, Tomáš Peitl will give a live demo of SMS and its QBF extension.

The enhanced performance of today’s MaxSAT solvers has elevated their appeal for many large-scale applications, notably in software analysis and computer-aided design. Our research delves into refining anytime MaxSAT solving by repeatedly identifying and solving with an exact solver smaller subinstances that are chosen based on the graphical structure of the instance. We investigate various strategies to pinpoint these subinstances. This structure-guided selection of subinstances provides an exact solver with a high potential for improving the current solution. Our exhaustive experimental analyses contrast our methodology as instantiated in our tool MaxSLIM with previous studies and benchmark it against leading-edge MaxSAT solvers.

We describe a family of CNFs in n variables which have small resolution refutations but are such that any small refutation must have height larger than n (even exponential in n), where the height of a refutation is the length of the longest path in it (a similar result appeared in [1]). Small refutations of our formulas are thus highly irregular, containing paths querying the same variable many times. This makes it a plausible candidate to separate resolution from pool resolution, which amounts to separating CDCL with restarts from CDCL without. We are not able to show this, but in the other direction we show that a simpler version of our formula, with a similar irregularity property, does have polynomial size pool resolution refutations.

In this talk, I presented the current state of the Isabelle/HOL mechanization efforts that I am leading on the “splitting framework”, that makes it possible to use propositional models and a SAT solver to guide the inferences of a saturation-based calculus, as is done in AVATAR. The Isabelle/HOL results do not cover AVATAR yet, but a simpler form of splitting. In ongoing work, we cover “splitting without backtracking” over resolution in FOL. The work was still ongoing at the time of the seminar and I explained where we stood then and why.

We discuss connections between SAT solvers and proof complexity: how we can analyse the CDCL algorithm thanks to resolution, and how stronger proof systems can guide new developments.

We study the algorithmic problem to enumerate all satisfying assignments of a given propositional formula. For formula classes with a polynomial-time decision problem, this can be done within the class DelayP, introduced by Johnson, Papadimitriou and Yannakakis in 1988 and regarded since then as a reasonable notion of “efficient” enumeration. We will present two results:

1. 1.

   We generalize the class DelayP to a hierarchy analogous to the polynomial-time hierarchy of decision problems and show that Enum-SAT is complete in the ${\mathrm{\Sigma }}_1$-level of this hierarchy under some form of enumeration Turing reductions.

2. 2.

   We define a hierarchy of very efficiently enumerable problems within DelayP, based in the Boolean circuit class AC₀, and place the enumeration problems for monotone, IHS, Krom, and affine formulas in lower levels of this hierarchy.

Open remains an exact classification of the problem Enum-Horn-SAT.