## sat_toasty_helper

A utility library for more-easily writing SAT constraints

### 3 releases

 0.0.3 Apr 6, 2024 Apr 6, 2024 Feb 27, 2024

#914 in Algorithms

MIT/Apache

21KB
360 lines

# sat_toasty_helper is a convenient way to write and solve SAT constraints in Rust

Currently, sat_toasty_helper relies on splr, a modern SAT solver written in Rust.

In the future, I hope to make this part more configurable - but for the initial release, it's provided to give the best "batteries-included" experience for initial setup.

This is a very WIP project; I'm gradually cleaning up and publishing pieces of the utilities I've built for setting and solving pen-and-paper puzzles.

## Sudoku

Here's an example of setting up Sudoku constraints (TODO: show usage as import of crate):

use sat::{Lit, Prop, Solver};
mod sat;

use sat::ClauseBuilderHelper;
use Lit::*;

// Define a type representing a position in the Sudoku grid.
// 0 <= r, c < 9.
#[derive(Copy, Clone, Eq, PartialEq, Hash, PartialOrd, Ord, Debug)]
struct GridCell {
r: i32,
c: i32,
}

/// We can define custom "propositions" (without interpretation) by addding an `impl Prop` for them.
/// The `Num(p, v)` proposition says that grid cell `p` contains the digit `v`.
#[derive(Copy, Clone, Eq, PartialEq, Debug, PartialOrd, Ord)]
struct Num(GridCell, i32);
impl Prop for Num {}

fn main() {
// Create a new solver. All of the constraints will be added to this object.
let mut s = Solver::new();

// Set up the rules for Sudoku:
let cells: Vec<GridCell> = (0..9)
.flat_map(|r| (0..9).map(move |c| GridCell { r, c }))
.collect();

// Each cell has a value.
for &p in &cells {
// This means that exactly one of Num(p, 1); Num(p, 2); ...; Num(p, 9) is true.
s.exactly_one((1..=9).map(|v| Pos(Num(p, v))));
}

// If two different cells share a row, column, or 3x3 box, they cannot have the same value.
for &p1 in &cells {
for &p2 in &cells {
if p1 == p2 {
continue;
}
if p1.r == p2.r || p1.c == p2.c || (p1.r / 3, p1.c / 3) == (p2.r / 3, p2.c / 3) {
for v in 1..=9 {
// They cannot both be 'v':
s.at_most_one([Pos(Num(p1, v)), Pos(Num(p2, v))]);
}
}
}
}

// Get the solution.
// In production code, you should check here for errors (timeouts or unsatisfiability).
let ans = s.solve_splr().expect("solvable").unwrap();

// Print the resulting grid:
for r in 0..9 {
for c in 0..9 {
let p = GridCell { r, c };
for v in 1..=9 {
// We can look up the `Var` for each proposition by calling `.resolve_prop`.
if ans[&s.resolve_prop(Num(p, v))] {
print!("{v}");
}
}
}
println!();
}
}

~590KB
~14K SLoC