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. Currently, I am exploring QBF pre-processing and proof optimization. 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 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.