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