Comment #8 on issue 1879 by christian.muise: Satisfiable theory resulting
in False
http://code.google.com/p/sympy/issues/detail?id=1879
The use of clauses rather than unknown clauses is definitely a bug. The
test case I
put in (f5) may pass in the 1545 branch, but I'm sure there's some
contrived example
that wouldn't :p. The fix here covers the bug in unit_propagate indirectly
(I think
both should go in) by making sure the new variable choice is added to the
model in
the recursive call.
As a separate issue, I'd like to rewrite the unit prop as a closure
anyways.
Typically one would use it to simplify the theory until no further unit
propagation
could occur -- it would allow unit_prop to be used as a stand alone
function rather
than just for the DPLL procedure.
--
You received this message because you are listed in the owner
or CC fields of this issue, or because you starred this issue.
You may adjust your issue notification preferences at:
http://code.google.com/hosting/settings
--
You received this message because you are subscribed to the Google Groups
"sympy-issues" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sympy-issues?hl=en.
