Updates:
Labels: -logic Logic NeedsReview
Comment #12 on issue 1545 by [email protected]: Efficient data
representation in logic.satisfiable()
http://code.google.com/p/sympy/issues/detail?id=1545
I've finally updated my patch, see
[http://github.com/rlamy/sympy/tree/DPll-perf].
I'm not satisfied with the way I handled known_facts_compiled, but this
should be
refactored, which a separate issue.
Performance improvements are modest for small problems but very significant
for large
ones. Here's an isympy benchmark using
[ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/benchmarks/cnf/bf0432-007.cnf.Z]:
In master:
----
In [1]: from sympy.logic.utilities import dimacs
In [2]: expr = dimacs.load_file('bf0432-007.cnf')
In [3]: syms = list(expr.atoms())
In [5]: from sympy.logic.algorithms.dpll import *
In [6]: ex2 = to_int_repr(conjuncts(expr), syms)
In [7]: s2 = range(1, 1+len(syms))
In [8]: %time dpll_int_repr(ex2, s2, {})
CPU times: user 58.78 s, sys: 0.06 s, total: 58.83 s
Wall time: 58.88 s
Out[9]: False
----
In my branch:
----
In [1]: from sympy.logic.utilities import dimacs
In [2]: expr = dimacs.load_file('bf0432-007.cnf')
In [3]: syms = list(expr.atoms())
In [4]: from sympy.logic.algorithms.dpll import *
In [5]: ex2 = to_int_repr(conjuncts(expr), syms)
In [6]: s2 = set(range(1, 1+len(syms)))
In [7]: %time dpll_int_repr(ex2, s2, {})
CPU times: user 3.06 s, sys: 0.00 s, total: 3.06 s
Wall time: 3.07 s
Out[8]: False
----
However the performance of to_int_repr() is horrible: it takes something
like 20
seconds in this case!
Ideas for further improvements:
- Fix to_int_repr (easily done: use a dict instead of list.index)
- Update the functions in sympy.logic.algorithms.dpll to use their
*_int_repr
counterpart. (However, I wonder whether find_unit_clause or
find_pure_symbol are
really useful)
- Possibly, turn the integer representation concept into an actual Python
class.
--
You received this message because you are listed in the owner
or CC fields of this issue, or because you starred this issue.
You may adjust your issue notification preferences at:
http://code.google.com/hosting/settings
--
You received this message because you are subscribed to the Google Groups
"sympy-issues" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sympy-issues?hl=en.
