Email: jereeves [at] cs [dot] cmu [dot] edu
CV
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.
My thesis proposal lays out several
avenues for improving SAT solving using cardinality constraints. The thesis focuses on
both solving and encoding techniques. Our paper on improved encodings will appear in AAAI 2025.
Research Publications and Talks
-
Joseph E. Reeves, João Filipe, Min-Chien Hsu, Ruben Martins, and Marijn J. H. Heule
The Impact of Literal Sorting on Cardinality Constraint Encodings (2025) [pdf-preprint]
To appear in AAAI [repo-pending, talk-pending]
-
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
Cardinality Constraints in Automated Reasoning (2024) [poster]
In NDSEG Fellowship Program Conference
Honorable Mention (runner up for Computer and Computational Sciences)
-
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.