Email: jereeves [at] cs [dot] cmu [dot] edu
About
Hello! My name is Joseph Reeves and I am a PhD student (began Fall 2020)
at Carnegie Mellon University advised by Marijn
Heule and Randy Bryant.
In the past, I have worked on projects that generate structured CNF benchmarks
and experimentally evaluate stateoftheart CDCL solvers.
I also worked with QBF preprocessing, moving definition variables to improve solver performance.
In general, I am interested in finding short explainable proofs
(focusing on the PR proof system) and automatically scheduling binary decision diagram (BDD)based solvers that generate proofs.
Research Publications and Talks

Joseph E. Reeves, Benjamin KieslReiter, and Marijn J. H. Heule
Propositional Proof Skeletons (2023) [pdf]
In TACAS [repo pending, talk: slides pending]

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
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.