minisat-rust

minisat-rust copied to clipboard

Hi, I am in over my head. But it comes up from time to time that cargo could use a SAT solver to get faster or more reliable results. And this is a pure rust SAT solver, so what would be involved in putting this on crates.io with an api for dynamically building up a problem? Then perhaps using it in cargo?

Hello! What kind of API you have in mind?

I've never put something on crates.io before, so I can't confidently answer that question :) Also I know nothing about inner workings of how cargo resolves dependencies.

So I don't know much about SAT solvers so I don't really know what the API should look like, but hear is a straw man.

extern crate minisat;
...

let mut s = minisat::Problem::new();
let x0 = s.new_var();
let x1 = s.new_var();
let x2 = s.new_var();
s.add_clause(&[x0, x1, x2]);
s.add_clause(&[x0, !x1]);
s.add_clause(&[x1, !x2]);
s.add_clause(&[x0, !x2]);
match s.solve() {
    Ok(solution) => println!("{:}", solution),
    Err(contradiction) => println!("{:}", contradiction),
}

Publishing on crates.io is surprisingly easy. See the doc at https://doc.rust-lang.org/cargo/reference/publishing.html

I also do not know how cargo resolves dependencies, but I am trying to figure it out. I think it is trying to solve a system of constraints.

1. Recursively all dependencies of all depended upon crates must be satisfied.
2. Can not have 2 or more semver compatible versions of the same crate.
3. Not yet implemented; Can not have 2 or more -sys crates that link to the same thing. Then, If there are multiple solutions to the system take the one with the newest releases.

This is exactly what it should look like. This is more or less standard minisat api, except minisat offers satisfying assignment as models and also supports incremental solving. Along with this, I will suggest some convenient functions like these.

There's a Rust crate that wraps the original minisat library that has basically this exact API: https://github.com/luteberget/minisat-rs

It also has a couple of convenient extensions (in Rust) such as the "Symbolic" API. The sudoku example in the README is a nice use case for that.

However being able to do this with a pure Rust solution would be awesome, so +1 to the idea.