Writing · tag
Encoding a 4x4 Sudoku as a propositional formula — cell, row, column and 2x2 constraints — and letting the limboole SAT checker solve it.