Doctoral Thesis Proposal - Joseph E. Reeves

— 12:30pm

Location:
In Person and Virtual - ET - Reddy Conference Room, Gates Hillman 4405 and Zoom

Speaker:
JOSEPH E. REEVES, Ph.D. Student, Computer Science Department, Carnegie Mellon University
http://www.cs.cmu.edu/~jereeves/

Cardinality Constraints in Satisfiability Solving

Automated reasoning (AR) engines solve problems represented in mathematics and logic stemming from a wide range of domains including hardware and software verification, cryptography, and cloud security. Boolean satisfiability (SAT) solvers drive much of the reasoning behind many AR engines, but their input format, a formula in propositional logic, can be limiting. High-level constraints must be encoded into sets of simpler constraints, clauses, and finding a good encoding often requires expert knowledge. We propose extending the input of SAT solvers to include cardinality constraints, moving encoding questions from the user-side to the solver-side. Cardinality constraints are a frequently occurring type high-level constraint that represent counting, e.g., “at least k packages must be delivered” or “you can work from home at most one day of the week”.

In this proposal we discuss four research problems arising from a cardinality-based input. First, we will develop a cardinality constraint extraction tool that will convert previously encoded problems into a cardinality-based normal form, providing backwards compatibility for our solving techniques. Second, we will engineer dynamic cardinality constraint encoding into the top-tier SAT solver CaDiCaL to improve performance on problems with many cardinality constraints. Third, we will explore the ways in which parallel solving techniques can leverage information within cardinality constraints to achieve better problem partitioning. Fourth, we will equip the extraction and solving with end-to-end proof checking through modifications to existing proof systems and proof checkers. Our goal in investigating these four research problems is to support the claim that a cardinality-based format should be the standard input format for modern SAT solvers.

Thesis Committee

Marijn Heule (Chair)
Randal Bryant
Ruben Martins
Armin Biere (University of Freiburg) 

Additional Information

In Person and Zoom Participation.  See announcement.

Event Website:
https://csd.cmu.edu/calendar/doctoral-thesis-proposal-joseph-e-reeves