Skip to content

elireisman/sudoku-z3-rs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

22 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

Playing with Z3 SMT Solver in Rust

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages