mishun / minisat-rust Goto Github PK
View Code? Open in Web Editor NEWExperimental minisat SAT solver reimplementation in Rust
License: Other
Experimental minisat SAT solver reimplementation in Rust
License: Other
Snake case is the official style for idiomatic Rust code.
First, thank you for this project, it is very nice to have a decent SAT solver in a modern language.
I think it would be interesting to have an API (in the library part) that allows one to plug a theory in the SAT solver (that is, some trait Theory
that is given a slice of the trail after each decision+propagations, and can propagate/add clauses/raise a conflict on its own). The trait (with a default empty implementation that does nothing) could look like:
enum TheoryResult {
Sat { propagations: Vec<Lit>, split_clauses: Vec<Clause> },
Conflict { conflict_lemma: Clause }
}
trait Theory {
/// check if given slice of newly decided/propagated literals compatible with theory
fn on_propagate(&mut self, slice: &[Lit]) -> TheoryResult;
/// check if full assignment is sat
fn final_check(&mut self, full_trail: &[Lit]) -> TheoryResult;
}
What do you think?
edit: the propagations
field should contain a Vec<(Lit, Clause)>
or something similar (each propagated lit must be backed by a theory lemma, could be potentially lazy but has to be there for conflict analysis). Also, a callback to be called upon backtracking is required.
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?
When I uncomment the unittest I get this:
running 1 test
test compare_with_minisat ... test compare_with_minisat has been running for over 60 seconds
test compare_with_minisat ... FAILED
failures:
---- compare_with_minisat stdout ----
ok (UNSAT): ./tests/cnf/uuf50-0979.cnf.gz 0.00830 0.02760 3.33
ok ( SAT): ./tests/cnf/uf20-084.cnf.gz 0.00272 0.00677 2.49
ok ( SAT): ./tests/cnf/uf20-0868.cnf.gz 0.00289 0.00564 1.95
ok ( SAT): ./tests/cnf/uf50-0878.cnf.gz 0.00278 0.01479 5.31
ok ( SAT): ./tests/cnf/uf50-0836.cnf.gz 0.00370 0.01066 2.88
ok (UNSAT): ./tests/cnf/uuf50-0729.cnf.gz 0.00372 0.01545 4.15
ok ( SAT): ./tests/cnf/uf50-0177.cnf.gz 0.00307 0.01782 5.80
ok (UNSAT): ./tests/cnf/uuf50-0355.cnf.gz 0.00322 0.02612 8.11
ok ( SAT): ./tests/cnf/uf50-0118.cnf.gz 0.00387 0.01785 4.61
ok ( SAT): ./tests/cnf/uf50-0783.cnf.gz 0.00282 0.01738 6.17
ok ( SAT): ./tests/cnf/uf50-0759.cnf.gz 0.00296 0.01860 6.28
ok ( SAT): ./tests/cnf/uf50-0694.cnf.gz 0.00330 0.01142 3.47
ok ( SAT): ./tests/cnf/uf20-0825.cnf.gz 0.00320 0.00423 1.32
ok ( SAT): ./tests/cnf/uf20-0525.cnf.gz 0.00319 0.00470 1.47
ok (UNSAT): ./tests/cnf/uuf50-0830.cnf.gz 0.00394 0.01850 4.69
ok ( SAT): ./tests/cnf/uf50-0804.cnf.gz 0.00338 0.01107 3.27
ok ( SAT): ./tests/cnf/uf50-0756.cnf.gz 0.00279 0.01489 5.33
ok ( SAT): ./tests/cnf/2bitmax_6.cnf.gz 0.00322 0.03890 12.09
ok ( SAT): ./tests/cnf/uf50-0207.cnf.gz 0.00373 0.01259 3.38
ok ( SAT): ./tests/cnf/uf50-096.cnf.gz 0.00361 0.01060 2.94
ok ( SAT): ./tests/cnf/uf20-0194.cnf.gz 0.00343 0.00418 1.22
ok ( SAT): ./tests/cnf/uf20-019.cnf.gz 0.00256 0.00413 1.61
ok ( SAT): ./tests/cnf/uf50-0493.cnf.gz 0.00344 0.01011 2.94
ok ( SAT): ./tests/cnf/uf20-0442.cnf.gz 0.00322 0.00401 1.25
ok ( SAT): ./tests/cnf/uf50-01000.cnf.gz 0.00307 0.01452 4.74
ok (UNSAT): ./tests/cnf/uuf50-0698.cnf.gz 0.00268 0.01151 4.29
ok ( SAT): ./tests/cnf/uf50-0300.cnf.gz 0.00318 0.01083 3.41
ok ( SAT): ./tests/cnf/uf50-0788.cnf.gz 0.00350 0.01125 3.21
thread 'compare_with_minisat' panicked at 'assertion failed: `(left == right)`
left: `467716`,
right: `467725`: Number of conflicts on ./tests/cnf/uuf250-01.cnf.gz
Stats { solves: 1, restarts: 1023, decisions: 563809, rnd_decisions: 0, conflicts: 467716, propagations: 20828802, tot_literals: 5844112, del_literals: 1814505 }', tests/minisat.rs:151:5
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace.
failures:
compare_with_minisat
test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out
error: test failed, to rerun pass '--test minisat'
It looks like there is (at least one) deviation from the minisat algorithm, perhaps.
Would you mind adding a license file to the repo?
Hi,
Out of curiosity, have you considered submitting minisat-rust to the upcoming SAT Competition? If nothing else, it may provide some interesting data points how minisat-rust compares to the C++ implementation of minisat. It might also stir up some more interest in your project, although I don't know for sure of course. Either way, it's just a thought.
All best wishes,
A
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.