Automated reasoning tools are used in a wide range of applications from hardware and software verification to mathematical discovery. The workhorses underpinning many of these tools are Boolean satisfiability (SAT) solvers. To use a SAT solver, a problem must first be encoded in propositional logic as a conjunctive normal form (CNF) formula. It may seem strange that a problem as complex as quantum circuit synthesis can be represented in CNF as a series of disjunctive constraints on variables that can either be true or false, and furthermore, that such a representation is useful. But, thanks to several decades of algorithmic advancements, SAT solvers implementing the conflict-driven clause learning (CDCL) algorithm can efficiently solve a plethora of hard problems that no other tool can handle.

The main drawback to CNF is that it requires the encoding of all high-level constraints, and this can be both difficult for a user to find an optimal encoding and the encodings themselves can prevent a solver from leveraging structural information from the constraints during solving. One of the most commonly occurring high-level constraints in SAT problems are cardinality constraints. A cardinality constraint on Boolean variables counts the number of true variables and compares the sum against a bound. Cardinality constraints arise any time a problem requires counting. For example, 'synthesize a quantum circuit with at most k swap gates", or "each value from 1 to 9 may appear at most once in every row of a Sudoku puzzle".

This thesis proposes a new standard input for SAT solvers: AtLeastK Conjunctive Normal Form (KNF), with native support for cardinality constraints, which is both easier to use and will help improve solver performance. We develop several methods that take advantage of cardinality information in the KNF format to improve solving. First, we explore how the meaning of new variables introduced in cardinality constraint encodings can be improved by exploiting the relationships between variables in the formula. Second, we implement native cardinality constraint propagation as an extension of a modern CDCL solver and show that the faster propagation is especially helpful on satisfiable problems. Third, we develop a method that uses information from cardinality constraint encodings to split a formula into thousands of independent components that can then be solved in parallel. To evaluate our KNF solving techniques, we developed cardinality constraint extractors that detect AtMostOne constraints and implicit ExactlyOne constraints transforming a formula in CNF to KNF. We used our extractor to convert thousands of benchmarks from the past two decades of SAT competitions into KNF and found that our KNF solving techniques improved solver performance on many of these problems. This work has culminated in an open sourced solver that has been used by several collaborators in mathematical discovery, artificial intelligence explainability, and hardware synthesis research.

128 pages

Thesis Committee:
Marijn J.H. Heule (Co-chair)
Randal E. Bryant (Co-chair)
Ruben Martins
Armin Biere (University of Freiburg)

Jignesh Patel, Interim Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Creative Commons: CC-BY (Attribution)

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu