[YICES-HELP] Yices all-sat for bitvectors
bruno at csl.sri.com
Mon Feb 8 11:07:41 PST 2010
filip at matf.bg.ac.rs wrote:
> we are trying to use Yices solver (via C API) for bitvector arithmetic in
> our research and we have detected a strange behavior when we are looking
> for all models. Here is an example.
> "Find all bitvector pairs nx, ny of given length such that nx + ny == 0."
> The problem is that the search slows down significantly with every next
> found model. Our algorithm does yices_assert(nx + ny == 0), and then
> iteratively does a yices_check(). For each assignment (nx = mx, ny = my)
> that is found we do a yices_assert for a blocking clause of the form (nx
> != mx || ny != my) and repeat to yices_check until unsatisfiability. It
> succesfully finds all models, it seems that there are no memory leaks, but
> it obviously slows down and the last 20% of the models are found very
> However, when we add a number of random blocking clauses (of the same form
> nx != mx || ny != my) a priori and reduce the problem to finding just the
> last 20% models, these 20% models are found much faster then the last 20%
> of the models in the search for all models. This seems counterintuitive,
> because once the search for all models finds the first 80% of the models,
> theoretically it should be in the same point where the second search
> starts (the condition and 80% of the blocking clauses asserted) and both
> should find the remaining 20% of the models equally fast.
> Any help, comment or advice is appreciated.
> Thank you.
> Filip Maric,
> Automated reasoning group, University of Belgrade
There's no simple explanation for this behavior, except that the
solver state is different in both cases. After you've asserted
80% blocking clauses without calling check, the solver contains
about 500 boolean variables. After you've done 200 calls to
assert + check + get_model, the solver contains close to 25000
Because of the way yices handles bit-vector equalities, it creates new
clauses and boolean variables on the fly. These are created when 'check'
is called, and the number of these clauses varies a lot depending on
the search ordering. So calling 'check' many times has the effect of
increasing the problem size significantly. which causes a slow down
compared to asserting more constraints upfront.
More information about the YICES-HELP