Here’s a collection of some brief tutorials about SAT solving, written as Google Colab notebooks (in Python) so that no specific software is necessary.
Each of these links goes to a document that you can view and edit but not save, so to make your saveable copy you need to click on “File” and then “Save copy to 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 executing it you should be ready to get your hands dirty with the exercise notebooks in the next section. You should probably do them in order!
Exercise Notebooks
- Small Ramsey SAT: a first hands-on introduction to SAT solving by computing small Ramsey numbers.
- Small Schur SAT: a second step into SAT solving by computing small Schur numbers.
- Non-monochromatic rectangles SAT: a third step into SAT solving by computing colored grids without monochromatic rectangles.
- Small Cages SAT: a fourth step into SAT solving by computing small cage graphs.
- Non-transitive dice SAT: a final boss! Finding small sets of non-transitive dice with SAT.