Search Results

Documents authored by Codel, Cayden

Document
DOI: 10.4230/LIPIcs.SAT.2026.4
Simplify, Order, Break, Repeat

Authors: Markus Anders, Cayden Codel, and Marijn J. H. Heule

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
Existing symmetry-breaking techniques for SAT constrain the search space without simplifying the formula. Lex-leader predicates, the most widely used approach, add global ordering constraints to remove symmetric solutions, but often at the cost of substantial formula blowup and large proofs. Moreover, they ignore structural properties of the formula, such as connectedness, that could enable stronger symmetry breaking. In this paper, we present a new algorithm that treats symmetry breaking not merely as a restriction mechanism, but as a simplification mechanism. Notably, it only adds unit and binary symmetry-breaking clauses, which enables strong formula simplifications. This can expose additional symmetries and in turn allows for multiple rounds of symmetry breaking. Crucially, we exploit connectivity in the formula’s graph representation, including the presence of cliques, to guide the order of symmetry breaking. We implemented our algorithm in the satsuma tool and evaluated it on a large set of benchmarks. As a preprocessing step for CaDiCaL, it improves PAR-2 scores by 22% on the SAT competition 2025 and by 12% on the SAT anniversary track. It also substantially outperforms lex-leader and orbitopal fixing while producing compact proofs.
Cite as

Markus Anders, Cayden Codel, and Marijn J. H. Heule. Simplify, Order, Break, Repeat. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{anders_et_al:LIPIcs.SAT.2026.4,
  author =	{Anders, Markus and Codel, Cayden and Heule, Marijn J. H.},
  title =	{{Simplify, Order, Break, Repeat}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.4},
  URN =		{urn:nbn:de:0030-drops-263109},
  doi =		{10.4230/LIPIcs.SAT.2026.4},
  annote =	{Keywords: Boolean satisfiability, symmetry handling, preprocessing, Schreier-Sims}
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.26
An End-To-End Verification of Keller’s Conjecture

Authors: James Gallicchio, Cayden Codel, Jeremy Avigad, and Marijn J. H. Heule

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract
In 1930, Keller conjectured that every gap-free tiling of ℝⁿ by n-dimensional unit cubes must contain cubes that fully share an (n - 1)-dimensional face. Keller’s conjecture holds for n ≤ 7 and fails for n ≥ 8. The final case, n = 7, was settled in 2020 using a mix of traditional and automated reasoning. The result was obtained by reducing the conjecture to a set of clique-existence problems, encoding those problems into propositional logic, breaking symmetries, and solving them with a SAT solver. In this paper, we present an end-to-end verification in Lean 4 of Keller’s conjecture for all dimensions. First, we simplify a prior reduction of Keller’s conjecture to the clique-existence problems. We then verify an improved SAT encoding of those problems, as well as some symmetry reasoning on the encoding. Throughout our work, we sought to maximize the synergy between interactive and automated techniques while minimizing human proof burden. In particular, the symmetry reasoning was split between Lean and a mechanically-checkable proof system, since neither was suitable on their own for verifying all of the symmetry reasoning. We discuss how and why we chose to split the reasoning across these systems based on their relative strengths and weaknesses.
Cite as

James Gallicchio, Cayden Codel, Jeremy Avigad, and Marijn J. H. Heule. An End-To-End Verification of Keller’s Conjecture. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{gallicchio_et_al:LIPIcs.ITP.2026.26,
  author =	{Gallicchio, James and Codel, Cayden and Avigad, Jeremy and Heule, Marijn J. H.},
  title =	{{An End-To-End Verification of Keller’s Conjecture}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.26},
  URN =		{urn:nbn:de:0030-drops-270008},
  doi =		{10.4230/LIPIcs.ITP.2026.26},
  annote =	{Keywords: Keller’s conjecture, the Lean theorem prover, SAT encodings, SAT solving, Trestle, formal verification}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.9
Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups

Authors: Eric Wang, Arohee Bhoja, Cayden Codel, and Noah G. Singer

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Graded unipotent Chevalley groups are an important family of groups on matrices with polynomial entries over a finite field. Using the Lean theorem prover, we verify that three such groups, namely, the A₃- and the two B₃-type groups, satisfy a useful group-theoretic condition. Specifically, these groups are defined by a set of equations called Steinberg relations, and we prove that a certain canonical "smaller" set of Steinberg relations suffices to derive the rest. Our work is motivated by an application for building topologically-interesting objects called higher-dimensional expanders (HDXs). In the past decade, HDXs have formed the basis for many new results in theoretical computer science, such as in quantum error correction and in property testing. Yet despite the increasing prevalence of HDXs, only two methods of constructing them are known. One such method builds an HDX from groups that satisfy the aforementioned property, and the Chevalley groups we use are (essentially) the only ones currently known to satisfy it.
Cite as

Eric Wang, Arohee Bhoja, Cayden Codel, and Noah G. Singer. Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.ITP.2025.9,
  author =	{Wang, Eric and Bhoja, Arohee and Codel, Cayden and Singer, Noah G.},
  title =	{{Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.9},
  URN =		{urn:nbn:de:0030-drops-246071},
  doi =		{10.4230/LIPIcs.ITP.2025.9},
  annote =	{Keywords: Group presentations, term rewriting, metaprogramming, proof automation, the Lean theorem prover}
}
Artifact
Software
DOI: 10.4230/artifacts.22467
EmptyHexagonLean

Authors: Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule

Abstract
Cite as

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, Marijn J. H. Heule. EmptyHexagonLean (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22467,
   title = {{EmptyHexagonLean}}, 
   author = {Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:29dc0e7145296997bcb1230b4e03cd14c8d75617;origin=https://github.com/bsubercaseaux/EmptyHexagonLean;visit=swh:1:snp:0e11d6564bd15317306605932e0acd87cf3d7f80;anchor=swh:1:rev:d7f798ffc8deabc2f3ca1ae36e92e0250e57c205}{\texttt{swh:1:dir:29dc0e7145296997bcb1230b4e03cd14c8d75617}} (visited on 2024-11-28)},
   url = {https://github.com/bsubercaseaux/EmptyHexagonLean/tree/itp2024},
   doi = {10.4230/artifacts.22467},
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.35
Formal Verification of the Empty Hexagon Number

Authors: Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
A recent breakthrough in computer-assisted mathematics showed that every set of 30 points in the plane in general position (i.e., no three points on a common line) contains an empty convex hexagon. Heule and Scheucher solved this problem with a combination of geometric insights and automated reasoning techniques by constructing CNF formulas ϕ_n, with O(n⁴) clauses, such that if ϕ_n is unsatisfiable then every set of n points in general position must contain an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17 300 CPU hours of parallel computation. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers ideas in discrete computational geometry and SAT encoding techniques by introducing a framework that connects geometric objects to propositional assignments. We see this as a key step towards the formal verification of other SAT-based results in geometry, since the abstractions we use have been successfully applied to similar problems. Overall, we hope that our work sets a new standard for the verification of geometry problems relying on extensive computation, and that it increases the trust the mathematical community places in computer-assisted proofs.
Cite as

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. Formal Verification of the Empty Hexagon Number. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{subercaseaux_et_al:LIPIcs.ITP.2024.35,
  author =	{Subercaseaux, Bernardo and Nawrocki, Wojciech and Gallicchio, James and Codel, Cayden and Carneiro, Mario and Heule, Marijn J. H.},
  title =	{{Formal Verification of the Empty Hexagon Number}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.35},
  URN =		{urn:nbn:de:0030-drops-207633},
  doi =		{10.4230/LIPIcs.ITP.2024.35},
  annote =	{Keywords: Empty Hexagon Number, Discrete Computational Geometry, Erd\H{o}s-Szekeres}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact