Skip to content

Latest commit

 

History

History
23 lines (17 loc) · 881 Bytes

README.md

File metadata and controls

23 lines (17 loc) · 881 Bytes

Z3 Sudoku Solver + Rust

This is just a toy to play with the Rust bindings for the Z3 SMT Solver.

Quick and dirty examples:

# From checkout root:

# Generate a board with random seed values and if the
# solver is SATisfied, present a legal solution.
# Note: can generate UNSAT boards that appear legal; retry if needed
$ cargo r

# Solve a known input board from simple text format (whitespace is ignored)
$ cargo r -- --input example.board

# Generate a board to solve with N random seed values.
# Note can generate UNSAT boards that appear legal; retry if needed
$ cargo r -- --generate 16

Screenshot:

Screen Shot 2022-09-18 at 4 47 19 PM