Comment #1 on issue 4075 by asmeu...@gmail.com: More efficient to_cnf
http://code.google.com/p/sympy/issues/detail?id=4075
The algorithm apparently works by adding new symbols to the expression. The
guarantee is made that the new expression is satisfiable if and only if the
original was, and by the same model. This is a little different than what
to_cnf does, so probably this should be a separate function, or a flag in
to_cnf. It would probably be a little surprising if to_cnf returned an
expression that is not exactly logically equivalent to the input, but this
is definitely what we need in the call to to_cnf in satisfiable().
The algorithm in the paper claims to be O(m), where m is the number of
operators (And(x, y, z) is counted as two operators). A modified algorithm
that efficiently handles duplicate subexpressions is O(m*log(m)). The naive
algorithm of distributing ands and ors is I believe O(2**m) (or something
like that). See for instance
https://en.wikipedia.org/wiki/Conjunctive_normal_form#Conversion_into_CNF.
--
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 sympy-issues+unsubscr...@googlegroups.com.
To post to this group, send email to sympy-issues@googlegroups.com.
Visit this group at http://groups.google.com/group/sympy-issues.
For more options, visit https://groups.google.com/groups/opt_out.
