> Also, satisfiable is called twice in the assumptions system, once to see
> if the expression can be true and once to see if it can be false.
>
I believe this can be done with only one call to satisfiability. Put the
expression into pl_true with any random interpretation. for eg.
pl_true(expr, {a1: True, a2: True, ... an:True}). Assume this gives the
value True, then check if the expr is Valid, if yes then you know it can't
be false, if no then the expr can be both true and false (under different
interpretations ofcourse). If pl_true gives False check if the formula is
unsatisfiable, if yes then it can't be true, if no then it can be both true
and false. This reduces the 2 SAT calls to 1 SAT call and 1 pl_true call.
--
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 sympy+unsubscr...@googlegroups.com.
To post to this group, send email to sympy@googlegroups.com.
Visit this group at http://groups.google.com/group/sympy.
For more options, visit https://groups.google.com/groups/opt_out.
