Updates:
Status: Invalid
Comment #8 on issue 1875 by christian.muise: Pure literal resolution and
unit propagation should coexist in the same closure loop
http://code.google.com/p/sympy/issues/detail?id=1875
Touche salesman, touche ;).
You're dead-on. Pure literals only remove clauses -- not remove literals
from
clauses. Marking as invalid. However, an argument can be made for running
the pure
literal detection prior to unit prop -- I'll test to see if this makes any
empirical
difference.
As for the failed cnf file -- it's due to the tabs in the input (as
supposed to
spaces). Looking at the branch for dpll using sets, I can't see any
difference in the
Dimacs interpreter (not sure how Ronan got it to run).
--
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.
