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 save-able 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.
Exercise Notebooks
-
Small Ramsey SAT: a first hands-on introduction to SAT solving by computing small Ramsey numbers. (Solution) -
Small Schur SAT: Use SAT to avoid monochromatic sums. (Solution) -
Non-monochromatic rectangles SAT: Ramsey theory on a grid: can you find structured solutions?. (Solution) -
Small Cages SAT: Find regular graphs of small girth. (Solution)
-
Non-transitive dice SAT: Which dice is better? Well, it's complicated... (Solution)