search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
324 stars 63 forks source link

Not able to found how to get different solution after every boolector_sat under same assertions #190

Closed gsingla21 closed 2 years ago

gsingla21 commented 2 years ago

Came across a BTOR_OPT_SEED option but it seems useless while running boolector_sat() multiple times. It shows the same result everytime. Want to get different result everytime boolector_sat() is executed through boolector_bv_assignment(). Is there any API that can I use to resolve it? I heard Picosat can enumerate all possible solutions without crutches. But how to get different or all possible sat solutions as output (could enumerate). I want to avoid extra assertions to negate the prev solution.

aniemetz commented 2 years ago

The seed passed via BTOR_OPT_SEED is internally only used for the local search engines, which are not enabled by default. Thus, it is expected that running boolector_sat() shows the same result every time. If you want to block models, you have to do this manually.