Email: jereeves [at] cs [dot] cmu [dot] edu
About
Hello! My name is Joseph Reeves and I am a PhD student (entered Fall 2020)
at Carnegie Mellon University advised by Marijn
Heule and Randy Bryant.
My research interests revolve broadly around satisfiablity (SAT) solving.
I have worked on finding short and explainable proofs within the
propagation redudnancy (PR) proof system, and developed a PR preprocessing
algorithm that appeared in several solvers in the 2023 SAT Competition.
I have also explored proof summarization in my proof skeletons work,
and am investigating ways to lift the core ideas to SMT solving.
For my PhD thesis, I am researching the ways in which we can leverage a
cardinality-based input to improve SAT solvers. The introductory paper
"From Clauses to Klauses" was presented at CAV 2024 (link below).
Research Publications and Talks
-
Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant
From Clauses to Klauses (2024) [pdf]
In CAV [repo, talk:slides]
-
Joseph E. Reeves, Benjamin Kiesl-Reiter, and Marijn J. H. Heule
Propositional Proof Skeletons (2023) [pdf]
In TACAS [repo, talk:slides]
-
Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant
Preprocessing of Propagation Redundant Clauses (2022) [pdf]
In IJCAR [repo, talk:slides]
-
Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant
Moving Definition Variables in Quantified Boolean Formulas - Talk (2022) [extended abstract]
In QBF workshop [repo, talk:slides]
-
Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant
Moving Definition Variables in Quantified Boolean Formulas (2022) [pdf]
In TACAS [repo, talk:slides]
-
Joseph E. Reeves and Marijn J. H. Heule
The Impact of Bounded Variable Elimination of Pigeonhole Formulas (2021) [pdf]
In Pragmatics of SAT [repo , talk:slides]
-
Cayden R. Codel, Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant
Bipartite Perfect Matching Benchmarks (2021) [pdf]
In Pragmatics of SAT [repo, talk:slides]
Software
Cardinality-CaDiCaL [repo] - the repository provides an extraction engine and solver configurations. The extractor transforms a formula in Conjunctive Normal Form (CNF) into a formula in Cardinality Conjunctive Normal Form (KNF). The solver is a modified version of CaDiCaL that takes as input a formula in KNF and applies one of three solving configurations: reencoding the cardinality constraints, propagating natively on the cardinality constraints, or a combination of both.
PReLearn [repo] - a preprocessor that extracts binary and ternary PR clauses from a CNF formula. These clauses can be added to the formula then passed to a SAT solver, with a general improvement in performance.
BiPartGen [repo] - generates a CNF for the perfect matching problem on bipartite graphs with random constructions and various at-most-one encodings. Additionally provides tools to produce symmetry-breaking clauses. A selection of formulas were submitted to the SAT competition 2021.