search

jix / varisat

SAT solver written in Rust
https://jix.one/project/varisat
Apache License 2.0
253 stars 17 forks source link

Support for multiple satisfiable assignments #86

Closed tsionyx closed 5 years ago

tsionyx commented 5 years ago

Is there a way to force the solver to find another set of assignments if it already has found one satisfiable set of variables?

jix commented 5 years ago

Yes, you can use incremental solving (just calling add_clause again after a call to solve to add a clause that blocks an already found solution). Calling solve after that will then find a different solution if it exists.

This is not the most efficient way, though. The solver itself could block a found solution in a more efficient way than currently possible, but that is not implemented yet. The issue for that is #22.

tsionyx commented 5 years ago

Thank you! I'll try it.