Accepted to SAT '25
SlidesIn this project, I used partial runs of CDCL SAT solvers and the proof prefixes which they generate in order to better select variables for use in the Cube and Conquer SAT solving paradigm. Our results outperform the existing state of the art tool, March, in many cases, especially on difficult combinatorial problems.
Used group theory and SAT solvers to find and verify the most adversarial board in the Keep Talking and Nobody Explodes module Hexamaze. A blog post detailing this project can be found here.
For my Advanced Topics in Principles of Programming Languages Class, I wrote a compiler for a fragment of ML based on a talk given by Max New. A full report, including detailed descriptions of the intermediate representations, proofs of correctness, as well as an implementation, can be found on my Github