Playground
A Sudoku solver and an SMT-LIB runner using Z3 in your browser. The engine loads on first use; the page may reload.
Sudoku
Eighty-one integer variables in 1–9, pairwise distinct per row, column, and box, with your givens pinned by equality. Pick a puzzle, edit any cell, then press Solve. The grid below is the only input.
Pick a puzzle or type your own, then Solve.
SMT-LIB
Pick a preset or write an SMT-LIB 2 script, then press Run.