Doctoral Thesis Oral Defense - Joseph Reeves
— 1:00pm
Location:
In Person and Virtual - ET
-
ASA Conference Room, Gates Hillman 6115 and Zoom
Speaker:
JOSEPH REEVES
,
Ph.D. Candidate
Computer Science Department
Carnegie Mellon University
https://www.cs.cmu.edu/~jereeves/
Automated reasoning is a branch of artificial intelligence that uses search engines called solvers to find solutions for problems formulated in mathematics and logic. Automated reasoning has been applied across a wide range of domains from hardware and software verification to mathematical discovery. To solve a diverse set of problems, these tools make use of low-level reasoning, namely the conflict-driven clause learning algorithm, which is made possible by first encoding a problem into low-level logic.
Encoding is pivotal to the success of a solver. High-level constraints are transformed into low-level logic via abstractions, and using a suboptimal set of abstractions might increase a solver’s runtime by factors of a hundred. In this thesis, we focus on one type of high-level constraint: cardinality constraints. Cardinality constraints appear in any problem that 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". It is standard practice to make users encode these constraints before passing them as input to an off-the-shelf solver.
We propose an extended input format that includes cardinality constraints. This allows us to move questions of encoding out of the hands of the user and into the domain of the solver. We present several techniques that leverage the structural information provided by this new input format to automatically generate more effective cardinality constraint encodings. Furthermore, we developed a new solver that employs cardinality-specific reasoning to quickly find solutions for problems from hardware synthesis and discrete mathematics
Thesis Committee
Randal Bryant (Co-chair)
Marijn Heule (Co-chair)
Ruben Martins
Armin Biere (University of Freiburg)
In Person and Zoom Participation. See announcement.
For More Information:
matthewstewart@cmu.edu