Comment #4 on issue 4075 by [email protected]: More efficient to_cnf
http://code.google.com/p/sympy/issues/detail?id=4075
Do you know of any better references for this, aimed more toward
implementation? It seems like in many (most?) cases, adding new variables
is unnecessary. For instance, if I have a conjunction of a bunch of
implications or double implications, that is basically already in cnf. As a
somewhat less trivial example, if I have Implies(p, x), where p is in dnf
and x is a variable, then the conversion is not so bad, because ~p is in
cnf, and you then just have to distribute the x to each term.
By the way, another question. If the input to satisfiable is an Or, would
it be more efficient to just recursively call satisfiable on each argument
until an answer is found? This seems like it might be more efficient than
converting it to cnf, especially since if it happens to be in dnf, then the
answer would be found instantly. Even if you have a huge Or that ends up
being unsatisfiable (the worst case), it still seems like this would be
more efficient than converting to cnf, at least given the current naive
to_cnf. But I didn't test it, so I could be wrong.
--
You received this message because this project is configured to send all
issue notifications to this address.
You may adjust your notification preferences at:
https://code.google.com/hosting/settings
--
You received this message because you are subscribed to the Google Groups
"sympy-issues" 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-issues.
For more options, visit https://groups.google.com/groups/opt_out.
