SAT for Mathematics
Tutorials
Here's a collection of brief SAT-solving tutorials, written as Google Colab notebooks in Python so that no local setup is necessary.
You can view and edit each notebook directly. To keep your own version, choose “File” and then “Save a copy in Drive” in the Colab menu.
Starting Point
To get started, the following notebook shows the basic usage of the PySAT library, with no exercises.
Introduction to PySAT
After this, you'll be ready to work through the exercise notebooks in the next section. We recommend doing them in order.
Exercise Notebooks
-
Small Ramsey SAT
A first hands-on introduction to SAT solving by computing small Ramsey numbers.
-
-
Non-monochromatic rectangles SAT
Ramsey theory on a grid: can you find structured solutions?
-
-
Boolean Erdős Discrepancy Problem via SAT
Recreate the solution to a long-standing open problem in a couple of minutes!
-
Kaplansky's Unit Conjecture via SAT
Recreate Giles Gardam's 2021 SAT-found counterexample to a conjecture that had stood open for 80 years.
-
