Notes: Markus and Marijn combined their respective expertise on symmetry breaking and SAT proof systems 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.