[YICES-HELP] Search space

[Bruno Dutertre]

Stephan Zimmer wrote:
> Dear all,
> 
> I'd like to ask one question which regards the boolean DPLL engine of yices: if I pass a large set of clauses (=> P C1), ..., (=> P Cn) to yices, where P is a propositional variable, and Ci clauses (including arithmeitcs), and additionally assert P to be false,  then the whole context is trivially satisfiable (a model is simply given by (not P)).
> 
> But, somehow in contrast to the intuition, yices needs a very long time to find this out, it seems that it is working on the formulae Fi even though this is not neccessary because a simply unit propagation step shows that P must be set to "false". What could be an explanation for this?
> 
> Thanks in advance.
> 
> Best,
> Stephan

Stephan,

That's correct. Yices has to assign a truth value to all
boolean variables including all formulas Fi's. There is no code
to detect whether or not Fi is relevant. So even though
P is false and all clauses are true, the search continues.

In your example, the cost is in finding consistent truth values
for a set of non-boolean formulas F_1 .... F_n. That can be expensive,
depending on what the formulas look like. Since Yices tries to build
a full model, this cost cannot be avoided altogether. Of course, if
it's known that the truth values of F_1 ... F_n do not really matter then
building a full model could be done cheaply. We'll investigate ways
of improving this in future versions of Yices.

The first version of Yices from 2005 maintained information about
relevant Boolean variables but that did not pay off overall in the
benchmarks we had at the time. It looks like we may need to put this
back.

Bruno