[YICES-HELP] Search space
st.zimmer at web.de
Fri Sep 7 01:31:30 PDT 2007
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.
Der WEB.DE SmartSurfer hilft bis zu 70% Ihrer Onlinekosten zu sparen!
More information about the YICES-HELP