mishun / minisat-rust Goto Github PK

View Code? Open in Web Editor NEW

71.0 2.0 6.0 9.97 MB

Experimental minisat SAT solver reimplementation in Rust

License: Other

Rust 100.00%

rust minisat sat-solver np-complete cnf

minisat-rust's People

Contributors

Stargazers

Watchers

Forkers

brohee graydon morganbauer koba-e964 fauxfaux dralley

minisat-rust's Issues

Use proper naming convention.

Snake case is the official style for idiomatic Rust code.

API to write SMT solvers

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.

Can this be made available as a library?

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?

Test failure?

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.

License?

Would you mind adding a license file to the repo?

SAT Competition

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

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.