Tutorial SAT-solving for Discrete Mathematics

            18th Conference on Intelligent Computer Mathematics
                                - CICM 2025 -
                             October 6-10, 2025
                               Brasilia, Brazil 
                     http://www.cicm-conference.org/2025

----------------------------------------------------------------------------------------
 ROOM: LaForCE
---------------------------------------------------------------------------------------- 
          
Based on a recent success at the AI for Mathematics and Theoretical Computer Science
workshop at the Simons Institute for the Theory of Computing, this half-day tutorial
is dedicated on the usage of SAT solvers as a computational tool to assist research
in discrete mathematics. The goal of the tutorial is to teach, through hands-on
experience, how SAT solvers can assist us in constructing examples and counterexamples
in discrete mathematics, finding the smallest structures that satisfy combinatorial
constraints, eliciting conjectures, etc. In a nutshell, whenever the (in)existence of
a combinatorial object can be described in propositional logic, a SAT solver might be
able to help! More concretely, the tutorial would start with a 45-minute introductory
talk, similar in spirit to my talk at the Simons Institute, “Computer-Assisted
Intuition: SAT Solvers in Mathematical Discovery”. Then, the core of the tutorial would
be a session of 3 hours, where assistants would get hands-on experience through 
a series of Python exercise notebooks, available at my personal website. The exercise
notebooks, co-authored with Marijn Heule, a world-renowned expert in the usage of SAT
solvers for mathematical problems, are structured in increasing order of difficulty
and independence:

1. An introduction to the PySAT library used throughout the tutorial.
2. An initial glimpse into Ramsey numbers through SAT.
3. An initial step into Schur numbers through SAT.
4. Constructing cages, small regular graphs without short cycles.
5. Grids without monochromatic rectangle corners, and the search for structured solutions.
6. Finding non-transitive sets of dice with SAT.

While knowledge of the Python programming language will certainly facilitate the tutorial,
it is not strictly required, since with some basic coding experience in any programming
language, and potentially some help from LLMs, I believe any mathematician could learn
successfully from this tutorial. I would be the sole organizer of this tutorial at CICM,
but the material for it has been co-authored with Marijn Heule, and benefited from
feedback of many assistants to the aforementioned workshop at the Simons Institute. 

Speaker

 Bernardo Subercaseaux/ Carnegie Mellon University