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
cardinalitybased input to improve SAT sovlers. 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 KieslReiter, 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
CardinalityCaDiCaL [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 atmostone encodings. Additionally provides tools to produce symmetrybreaking clauses. A selection of formulas were submitted to the SAT competition 2021.