Computer Science PhD candidate at Carnegie Mellon University

Bernardo Subercaseaux

I am a PhD candidate at CMU, where I am advised by the amazing Marijn Heule. I think mostly about using SAT for mathematics, but to be honest, I just love computer science and discrete mathematics in their full diversity.

Bernardo Subercaseaux in profile
Figure 1: me (hover for surprise).

Research statement.

I am passionate about several topics in discrete mathematics and theoretical computer science. My current focus is the intersection between automated reasoning (especially SAT solving) and mathematics. I also have significant experience in theoretical explainability and interpretability in AI, online algorithms, and combinatorial games.

  • SAT encodings. What are limits and possibilities of CNF encodings? How do we design encodings that perform well on actual SAT solvers?
  • Computers doing mathematics. The LLM avalanche is pressing us against the wall with questions about the future of mathematics, and I want to engage with them seriously.
  • Good side quests. Wordle, Mastermind, explainable AI, online algorithms, geometric puzzles and others; I like working on problems that refuse to let me go.

Lately, on paper.

  1. March 2026 Near-Optimal Encodings of Cardinality Constraintswith Andrew Krapivin and Benjamin Przybocki; it begins with SAT encodings and somehow ends at a fifty-year-old circuit problem.
  2. March 2026 Automated Reencoding Meets Graph Theorywith Benjamin Przybocki and Marijn Heule; we ask graph theory what a reencoding tool is really doing—and where it must eventually get stuck.
  3. January 2026 Price of Locality in Permutation Masterminda solo excursion into whether TikTok influencers are chaotic enough.
All papers, abstracts, and BibTeX →