Notes: James upgraded Trestle and Joshua Clune’s Lean formalization and paper to build the first end-to-end formalization of Keller’s conjecture. In 1930, Keller conjectured that every tiling of the n-dimensional space with hypercubes must contain two cubes that fully share an (n - 1)-dimensional face. The conjecture then spawned a fair bit of follow-up work; see the paper for more details. Here, James simplified Clune’s reduction to SAT, verified the SAT encoding, and ran SAT solvers against a verified proof checker. I helped develop a few parts of Trestle crucial for the proof and co-wrote the paper.
Notes: This work is a spiritual successor to “Orbitopal Fixing in SAT.” Here, Markus developed a new symmetry-breaking technique that alternates between CNF formula simplification and symmetry breaking. In addition to using orbitopal fixing, the technique uses cliques in the formula’s variable-clause graph to guide which variables to fix. Experimentally, the technique boosts CaDiCaL’s performance by about 15%, and we submitted a solver based on our technique to the 2026 SAT Competition.
Notes: Recipient of a Distinguished paper award. Markus and Marijn joined forces at Dagstuhl seminar 25231 to develop new symmetry-breaking techniques for SAT that produce succinct SR proofs. I updated the SR proof checker dsr-trim, ran the experiments, and co-wrote the paper.
Notes: In a paper on arXiv, Noah proved by hand that a strictly-smaller set of the so-called Steinberg relations can be used to define an important family of groups. This result is key for constructing topologically-useful objects called higher-dimensional expanders. Noah’s proof required 80 pages of tedious calculations; this Lean verification was a good next step. Undergraduate students Eric and Arohee did the bulk of the formalization work in Lean. I acted as a technical advisor and helped automate the proofs.
Notes: This work is the spiritual successor to similar SAT proof checking tools such as drat-trim, dpr-trim, and cake_lpr. In this work, we introduce a more-general proof system called substitution redundancy, and we wrote an unverified checker in C (i.e., dsr-trim) and a verified checker in Lean (i.e., Trestle).
Notes: The eDRAT project began as a project involving Hanna, Bruno, Marijn, and myself while I was an intern with the Automated Reasoning Group at AWS during the summer of 2022. Hitarth and Bruno continued to work on the project the next summer. Hitarth gave the research talk.
Notes: This project was a Lean formalization of the pen-and-paper + SAT solving result made by my advisor earlier in 2024. I worked mainly with James on the infrastructure around verified encodings, which are a feature of the Trestle project. Mario gave the research talk.
Notes: A tool paper for work done on “A Linear Weight Transfer for Local Search.”
Notes: Conference paper of my master’s thesis of very similar name. I have given several versions of this talk, including one at FMCAD, one at CanaDAM 2023, and one at a Dagstuhl seminar on SAT encodings.
Notes: A continuation of work on the Divide and Distribute Fixed Weights (DDFW) algorithm, led by Solimul. See my thesis from 2021.
Notes: Unpublished master’s thesis. Completed for the partial fulfillment of a master’s degree in computer science at Carnegie Mellon University. Marijn Heule (chair), Jeremy Avigad, Bryan Parno, committee. This work has been continued in the Trestle project.
Notes: Unpublished undergraduate thesis. Completed for the fulfillment of undergraduate honors while at Carnegie Mellon University. My work received runner-up for the Allen Newell Award for Excellence in Undergraduate Research. A shortened version of the thesis was accepted to Pragmatics of SAT 2021, where I gave a talk.
Notes: This work extended a project from a special topics course taught by my advisor, Marijn Heule. The talk at Pragmatics of SAT 2021 was given by my co-author, Joseph Reeves.
Notes: I worked with the MineRL team for 18 months. While with them, I helped them develop code to allow AI agents to communicate with Minecraft, and I worked on experiment design and the data collection pipeline. The MineRL team has yearly competitions for increasingly harder tasks in the Minecraft video game.