Email: jereeves [at] cs [dot] cmu [dot] edu


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


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.