[YICES-HELP] Search space

[Stephan Zimmer]

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

_____________________________________________________________________
Der WEB.DE SmartSurfer hilft bis zu 70% Ihrer Onlinekosten zu sparen!
http://smartsurfer.web.de/?mc=100071&distributionid=000000000066