Comment #9 on issue 1875 by ronan.l...@gmail.com: Pure literal resolution and unit propagation should coexist in the same closure loop
http://code.google.com/p/sympy/issues/detail?id=1875

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).

Oh, I had forgotten about that. I just opened the dimacs file with an editor and
replaced all tabs with spaces.

--
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 sympy-iss...@googlegroups.com.
To unsubscribe from this group, send email to 
sympy-issues+unsubscr...@googlegroups.com.
For more options, visit this group at 
http://groups.google.com/group/sympy-issues?hl=en.

Reply via email to