SAT Encodings and Beyond

SAT is a powerful tool for solving a wide array of problems, but many problems are not expressed in propositional logic and must instead be encoded into SAT. These encodings are often subtle, and implementations are error-prone. Formal correctness proofs are needed to ensure that implementations are bug-free.

In this talk, we present a library for formally verifying SAT encodings, written using the Lean interactive theorem prover. Our library currently contains verified encodings for the parity, at-most-one, and at-most-k constraints. It also contains methods of generating fresh variable names and combining sub-encodings to form more complex ones, such as one for encoding a valid Sudoku board. The proofs in our library are general, and so this library serves as a basis for future encoding efforts.

Many hard combinatorial problems involve huge numbers of symmetries which derive from isomorphic representations of objects in the search space. Restricting search to avoid symmetries – aka “symmetry breaking” – makes a big difference when trying to solve such problems.

Symmetry breaking in constraint programming is often achieved by introducing symmetry breaking constraints which are satisfied by at least one member of each isomorphism class. Complete symmetry breaking constraints are satisfied by exactly one member from each class and other symmetry breaks are called partial.

In this talk I will focus mainly on breaking symmetries in graph search problems. The search for complete symmetry breaking constraints for graph search problems is itself a hard problem and it is unknown if there exists a complete symmetry breaking constraint that is polynomial in the size of the graph.

In computer science when the problem is hard – we typically follow one or more from three alternatives: (1) clever brute force computation, (2) approximation algorithms, or (3) identifying special cases where the problem is easier.

This talk will focus on how each of these three alternatives comes into play when solving hard graph search problems.

In this talk, we will discuss some results and some research directions that connect the theory of parameterized complexity and the theory of encodings and solvers for SAT and related problems such as ASP.

The talk can be divided into roughly two parts. The first part addresses the (im)possibility of fixed-parameter tractable encodings into SAT. This makes sense for problems whose (classical) complexity is beyond NP, and so one does not hope for polynomial-time encodings. For suitable choices of parameters, the problem could be encoded in fpt-time to SAT. We will give a few examples of cases where this is possible, and we present a parameterized complexity toolbox that can be used to assess the (im)possibility of fpt-time encodings into SAT.

The second part addresses an ongoing research direction, that revolves around encoding fpt-time solvable problems into SAT in such a way that CDCL solvers are guaranteed to run in fixed-parameter tractable time. For some problems, one can do this in such a way that this works with any branching heuristic, and for some problems the choice of branching heuristic makes a difference. We will present some examples illustrating this (for SAT and ASP), and then we raise some open research questions in this arena.

Product configuration has been among the first successful applications of symbolic AI, e.g. translating feature models with cross-tree constraints to SAT encodings and finding consistent solutions. Despite the high maturity of state-of-the-art tools, encoding remains challenging in practice: dynamic size (i.e. unbounded multiplicities of variables and constraints), OO-like inheritance (for clearer knowledge representation), open domains, merging of subsystem encodings (from distributed authors), multi-dimensional optimization, reconfiguration and knowledge evolution, explanations and recommendations, debugging, etc.

A common approach in automated reasoning is to encode a given problem into propositional logic and then solve the resulting formula with a satisfiability (SAT) solver. As the quality of the encoding has a big impact on solver performance, it is no coincidence that solvers are highly successful in the field of hardware verification: digital electronic circuits have a direct encoding into propositional logic which is often adequate for solving. However, the same is not true for many other applications. Sophisticated encodings may be required to efficiently solve some problems using SAT solvers. This talk will focus on sophisticated encodings of some hard-combinatorial problems for which a straightforward encoding is ineffective. We will first describe general techniques to produce high-quality encodings. Afterward, we will present encodings for specific problems: edge-matching puzzles, Hamiltonian cycles, and packing colorings.

Judgment aggregation (JA) offers a generic formal logical framework for modeling various settings where agents must reach joint agreements through aggregating the preferences, judgments, or beliefs of individual agents by social choice mechanisms. In this work, we develop practical JA algorithms for outcome determination by harnessing Boolean satisfiability (SAT) based solvers as the underlying reasoning engines, leveraging on their ability to efficiently reason over logical representations incrementally. Concretely, we provide algorithms for outcome determination under a range of aggregation rules, using natural choices of SAT-based techniques adhering to the computational complexity of the problem for the individual rules. We also implement and empirically evaluate the approach using both synthetic and PrefLib data, showing that the approach can scale significantly beyond recently proposed alternative algorithms for JA.

Encoding constraints to CNF is an attractive option for CP solvers, especially in the context of clause learning. However, it is not always a preferable or even feasible option, depending on our requirements. In this talk, I will go over some cases where SAT encodings have been used successfully in CP solvers, as well as some cases where it does not work out as well. I will point out some theoretical work for why this is the case, as well as some practical reasons for it.

Verifying multiplier circuits is an important problem which in practice still requires substantial manual effort. In this talk, I will demonstrate that encoding the entire problem into SAT is not the ideal strategy, nor is using a pure algebraic encoding. We use a combination of SAT and computer algebra in our method to significantly improve automated verification of integer multipliers.

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. SMS supports DRAT proofs for the SAT solver’s reasoning and offline verification of the symmetry breaking clauses, and thus provides an additional layer of confidence in the obtained results. This talk will discuss the basic concepts of SMS and review some of its applications on graphs, digraphs, hypergraphs, and matroids. At the end of the talk, we will give a live demo of the tool.

The performance of a constraint model can often be improved by converting a sub-problem into a single table constraint, which is referred to as tabulation. In this talk, I will describe an automatic tabulation approach, implemented in Savile Row which is a constraint model reformulation tool. Savile Row takes as input a model described in the high-level solver-independent modelling language Essence Prime and has backends for CP, SAT and ILP solvers. Our approach to automatic tabulation deploys heuristics to discover opportunities for tabulation and uses a specific propagator or an encoding for the generated table constraint depending on the chosen backend solver.

This work describes the UniCorT tool designed to solve university course timetabling problems specifically tailored for the 2019 International Timetabling Competition (ITC). The proposed approach includes pre-processing, the use of a maximum satisfiability (MaxSAT) solver and a local search procedure. The impact of a handful of techniques in the quality of the solution and the execution time is evaluated. We take into account different pre-processing techniques and CNF encodings, as well as the combination with a local search procedure. The success of our tool is attested by having been ranked among the five finalists of the ITC 2019 competition.

In the literature, there are several results making SAT-encodings and Boolean circuits. In particular, it is known that different classes of circuits correspond tightly to encodings with specific properties, e.g. restricted (tree/clique-)width or propagation strength. In this talk, I will survey some of these connections and point out some open questions.

The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general. This is joint work with Stephan Gocht, Ruben Martins and Jakob Nordström published at SAT’22.

We present a new SAT-based method for generating all graphs up to isomorphism that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry (SMS) framework with a technique that we call co-certificate learning. If SMS generates a candidate graph that violates the given co-NP property, we obtain a certificate for this violation, i.e., a “co-certificate” for the co-NP property. The co-certificate gives rise to a clause that the SAT solver serving as SMS’s backend learns as part of its CDCL procedure. We demonstrate that SMS plus co-certificate learning is a powerful method that allows us to improve the best-known lower bound on the size of Kochen-Specker vector systems, a problem that is central to the foundations of quantum mechanics and has been studied for over half a century. Our approach is orders of magnitude faster and scales significantly better than a recently proposed SAT-based method.

This talk is based on two papers about computing shortest resolution proofs of formulas in CNF, in which we investigate encodings to compute shortest proofs of minimally unsatisfiable formulas, and of hitting formulas in particular, we compute the hardest formulas (and the hardest hitting formulas) with a small number of clauses, and discuss related questions. The abstracts of the two papers follow.

1. 1.

   A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. In this paper, we introduce resolution hardness numbers; they give for m=1,2,… the length of a shortest proof of a hardest formula on m clauses. We compute the first 10 resolution hardness numbers, along with the corresponding hardest formulas. To achieve this, we devise a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for hardest formulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.

2. 2.

   Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands in stark contrast with other polynomial-time decidable classes, which usually have algorithms based on backtracking and resolution and for which model counting remains hard, like 2-SAT and Horn-SAT. However, those resolution-based algorithms usually easily imply an upper bound on resolution complexity, which is missing for hitting formulas. Are hitting formulas hard for resolution?

   In this paper we take the first steps towards answering this question. We show that the resolution complexity of hitting formulas is dominated by so-called irreducible hitting formulas, first studied by Kullmann and Zhao, that cannot be composed of smaller hitting formulas. However, by definition, large irreducible unsatisfiable hitting formulas are difficult to construct; it is not even known whether infinitely many exist. Building upon our theoretical results, we implement an efficient algorithm on top of the Nauty software package to enumerate all irreducible unsatisfiable hitting formulas with up to 14 clauses. We also determine the exact resolution complexity of the generated hitting formulas with up to 13 clauses by extending a known SAT encoding for our purposes. Our experimental results suggest that hitting formulas are indeed hard for resolution.

The SAT-based Local Improvement Method (SLIM) framework has yielded several competitive heuristics for a wide variety of problems such as treewidth, branchwidth, treedepth, decision trees, graph coloring, circuit minimization, etc. SLIM starts off with an initial heuristic solution and then repeatedly replaces small local parts with an improved version. The improved version is found by solving a SAT/MaxSAT/SMT encoding of the local part. This encoding must also ensure that the improved local part is still compatible with the rest of the global solution. We call this property ’replacement consistency’, and this is the key challenge in each SLIM instantiation. SLIM capitalizes on the scalability of the initial heuristic algorithm and the power of modern SAT solvers to produce heuristic solutions of higher quality than simpler local search techniques. In this talk, we give an overview of the SLIM framework and then discuss some case-studies demonstrating the application of SLIM.

Point and lines are fundamental entities from geometry. We discuss Erdös-Szekeres type problems on point sets and the underlying combinatorics of point configurations and their dual structure: arrangements of lines. By slightly relaxing the geometric restrictions (“lines” dont have to be straight), we obtain so-called pseudopoint configurations and arrangements of pseudolines. While the original settings cannot be axiomized via finitely many forbidden subconfigurations unless P=NP=ETR, there are indeed purely combinatorial descriptions for “pseudo” settings which allow to make investigations using computer assistance, and in particular, using SAT.

In this talk, we will have a closer look at solutions of quantified Boolean formulas (QBFs), i.e., the tree models of true QBFs and the tree counter-models of false QBFs and their representations as Boolean functions. These models and counter-models are of practical interest as they contain the solutions to the application problems encoded as QBFs. We will discuss how well-understood concepts from SAT like model enumeration and model counting transfer to QBF and their (counter-)models.

The MiniZinc modelling language lets users express their constraint satisfaction and optimisation problems in a high-level, solver-independent way. MiniZinc supports a range of decision variable types (integer, Boolean, set, float), container types (sets, arrays, tuples, records), and a large number of pre-defined predicates and functions for typical problem domains such as scheduling, packing, rostering, network problems and many others. A MiniZinc program (usually called a “model”) typically represents an entire problem class, which can be turned into a concrete problem instance by supplying values for the parameters defined by the program. MiniZinc can translate problem instances into input suitable for a variety of back-end solving formalisms, including CP (Constraint Programming), MIP (Mixed Integer Linear Programming), and SAT/MaxSAT (Boolean Satisfiability). The MiniZinc system consists of a generic, back-end independent compiler/interpreter implemented in C++, and back-end specific libraries of encodings expressed in the MiniZinc language itself. This talk will cover the basic architecture of the MiniZinc translation process, and then focus on the encodings for SAT, MaxSAT and QUBO, before giving a brief outlook on the next major version of MiniZinc that is currently under development.

I will describe two different ways of encoding Collatz-like problems into termination of string rewriting: one using a unary representation of integers and another using a mixed-base representation. When integers are represented in unary, the termination problem that corresponds to the Collatz conjecture (or even its simpler variants) does not admit proofs via natural matrix interpretations, a method widely used in proving termination of rewriting. I will sketch a proof of this impossibility result and then show a few instances where simply changing the encoding results in the termination problem becoming easy to solve (even automatically) via matrix interpretations.