Comment #9 on issue 1879 by [email protected]: Satisfiable theory resulting in False
http://code.google.com/p/sympy/issues/detail?id=1879
I guess you're probably right (since I can't prove you're wrong). But this is related to a bigger issue: there shouldn't be any known True clauses and the algorithm shouldn't have to inspect the model. Your change is half of a solution to this, the other being to unit-propagate the contents of the given model at the start of the algorithm. That way, clauses and symbols would only ever contain unassigned literals and the calls to pl_true can be replaced by checking whether the clause is empty.
-- 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.
