Status: New Owner: ---- Labels: Type-Defect Priority-Medium
New 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 In the DPLL implementation, both unit propagation and pure literal detection should be iterated until no more exist. The section marked "#compute DP kernel" may finish with unit clauses remaining. One potential solution would be to rewrite the unit propagation algorithm to follow the traditional meaning in the literature -- iteratively detect and propagate unit clauses. This way you would only need to call the function once, and again for each pure literal detected. This should also have an impact on the performance of the reasoner -- any sound propagation that can be done saves unnecessary decision points in the DPLL search space. To that end, it would be great if Fabian could attach some examples used to benchmark the DPLL performance. Anything that currently takes about 10 seconds to solve would be ideal. If this sounds like a reasonable idea, let me know and I'll create a branch and post the results here. -- 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.
