Comment #5 on issue 4075 by christian.muise: More efficient to_cnf
http://code.google.com/p/sympy/issues/detail?id=4075
Better references? There should be, but I just know it as general lore
around the SAT solving community. Your best bet is to analyze the types of
input you are expecting -- if it's more towards DNF, then flatten to that
and use model enumeration to solve your query. If it's more towards CNF,
then flatten to that and use a SAT solver. If it really is stuck half-way
in between (and flattening to either causes a combinatorial explosion),
then what I've seen is either Tseiten encodings or circuit solvers. The
former introduces the new variables, and the latter just runs DPLL on top
of the arbitrary formula.
Because flattening is a recursive procedure, it shouldn't be so hard to
create a DP that estimates the final CNF (or DNF) size without actually
computing it. That could be used at run time to determine what technique is
best.
--
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.
