SAT-Based Puzzle Solvers
Two puzzles reduced to Boolean satisfiability and solved with off-the-shelf SAT
solvers via PySAT: Sudoku (9×9) and Sokoban (parameterised grid).
The exercise is in the encoding — once the puzzle is a CNF formula, the
solver does all the search.
- Timeline
- Aug 2025 · CS228 Logic in Computer Science, IIT Bombay
- Instructor
- Prof. S. Krishna
- Language
- Python 3 · ~1,580 LOC across the CS228 assignments
- Stack
PySAT—CNF()+Solver(name='glucose3')·tester.py/test.pyharnesses- Scope
- Q1 Sudoku (729 vars) · Q2 Sokoban (time-indexed planning) · 6 clause families
- Repo
- github.com/.../CS228-Logic/Assignments/Assignment%201
Q1 — Sudoku as SAT
The 9×9 board needs 729 Boolean variables — one per
(row, col, digit) triple — with the mapping
id = 100·i + 10·j + k for readability. From there the constraints write
themselves:
- Cell coverage & uniqueness — each cell holds exactly one digit.
- Row, column, and 3×3 subgrid — each digit appears at least once and at most once in each.
- Given clues — every pre-filled cell becomes a unit clause that
pins its variable to
true.
Strictly, the "at most one" clauses are logically redundant — they're
implied by "at least one" plus the cell-uniqueness constraint via pigeonhole. They
were added anyway because helping the solver beats being elegant:
redundant constraints prune the search tree faster. Solved with
Solver(name='glucose3').
Q2 — Sokoban as SAT
Sokoban is a planning problem: push boxes onto goal tiles without pulling, without squeezing into corners. Encoding it requires time as a dimension.
State variables are time-indexed:
var_player(x, y, t) and var_box(b, x, y, t). The plan
horizon T is fixed up front and the encoder emits six families of
clauses:
- Initial state — player and boxes start at their given cells.
- Player movement — at step
t, the player moves to an adjacent free cell, with action-precondition constraints. - Box pushing — a box moves only when the player walks into it and the cell behind is free.
- Non-overlap — no two boxes in one cell; no player/box/wall overlap.
- Goal conditions — every goal tile holds a box at step
T. - Uniqueness / existence — the player is in exactly one cell at each step; each box has exactly one position.
Solved with Solver(name='g3'). The interesting engineering was the
variable-ID arithmetic — assigning each
(entity, position, time) tuple a globally unique positive integer
without collisions across the player and box variable spaces.
What I'd carry forward
Two lessons. First: declarative encoding makes the essence of the problem visible in a way procedural search doesn't — every constraint is named, and the solver tells you when you've under-specified the problem. Second: redundant clauses that look like noise to a human are often load-bearing for the solver. Logical minimality and search-tree minimality point in different directions.