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

Full list of publications can be found here: CV

About

Hello! My name is Joseph Reeves and I am a PhD student (entered Fall 2020) at Carnegie Mellon University advised by Marijn Heule and Randy Bryant with an anticipated graduation of December 2025.

My research interests revolve broadly around automated reasoning tools, though I have worked mostly with Boolean satisfiablity (SAT) solvers and satisfiability modulo theories (SMT) solvers. My recent projects have focused on four aspects of automated reasoning: (1) ease-of-use: using richer input formats to make tools more accessible; (2) stronger reasoning: automating the application of stronger reasoning techniques; (3) trustworthy solving: speeding up proof-producing SMT frameworks; and (4) explainable reasoning: summarizing and shrinking proofs to extract meaning.

My PhD thesis, Cardinality Constraints in Boolean Satisfiability Solving, has explored the ways in which we can leverage a cardinality-based input to improve SAT solvers. The goal of this research agenda is to move quesions about solving and encoding from the hands of users into the domain of the solver, both improving performance and making the tools more accessible to non-experts. The introductory paper "From Clauses to Klauses" was presented at CAV 2024. My thesis proposal lays out several avenues for improving SAT solving using cardinality constraints. We have three follow-up papers in AAAI, and SAT that show how encodings can be automatially improved as well as provide a mechanism for parallelizing solving with cardinality constraints.

Research Publications and Talks

Software

ulc-CaDiCaL [repo] - the repository provides an implementation of our ULC extraction and alignment algorithm as a preprocessing module inside of CaDiCaL.

Cardinality-CaDiCaL [repo] - the repository provides an extraction engine and solver configurations. The extractor transforms a formula in Conjunctive Normal Form (CNF) into a formula in Cardinality Conjunctive Normal Form (KNF). The solver is a modified version of CaDiCaL that takes as input a formula in KNF and applies one of three solving configurations: reencoding the cardinality constraints, propagating natively on the cardinality constraints, or a combination of both.

PReLearn [repo] - a preprocessor that extracts binary and ternary PR clauses from a CNF formula. These clauses can be added to the formula then passed to a SAT solver, with a general improvement in performance.

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.