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 state-of-the-art CDCL solvers.
I also worked with QBF pre-processing, 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 Kiesl-Reiter, 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 at-most-one encodings. Additionally provides tools to produce symmetry-breaking clauses. A selection of formulas were submitted to the SAT competition 2021.