In many (most???) cases the (un)satisfiability is of greater importance
than the satisfying expression (eg. validity, entailment). For all such
operations switching to a Semantic
Tableaux<http://en.wikipedia.org/wiki/Method_of_analytic_tableaux>seems to be
giving results MUCH faster than the previous method. Still
haven't run comparison with Tseitin, but this method, theoretically and
practically should give better results. Ofcourse, to find a model one would
still need the SAT solver.
Secondly, pl_true(a >> (b >> a), {}) would return None. Even though expr is
a tautology. The fact that pl_true cannot do the same is mentioned in the
comments. Using some extra time (proportional to the number of clauses), we
can return the actual result not just for tautologies but for all
expressions under partial interpretation. Is the correct answer worth the
extra time? Ofcourse we can modify the function into pl_true(expr,
deep=False) and do the above computation only if the user wants the exact
result.
--
You received this message because you are subscribed to the Google Groups
"sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sympy.
For more options, visit https://groups.google.com/groups/opt_out.
