I did not delete any methods, but added new ones with _int_repr suffix. dpll_satisifiable uses by default integer representation.
This represents a performance boost for all functions that make use of sympy.logic.satisfiable (e.g. query and refine module) --- sympy/logic/algorithms/dpll.py | 141 +++++++++++++++++++++++++++++++++-- sympy/logic/boolalg.py | 36 +++++++++- sympy/logic/inference.py | 4 +- sympy/logic/tests/test_boolalg.py | 12 ++- sympy/logic/tests/test_inference.py | 39 +++++++++- 5 files changed, 214 insertions(+), 18 deletions(-) diff --git a/sympy/logic/algorithms/dpll.py b/sympy/logic/algorithms/dpll.py index ee534c4..7fd09c0 100644 --- a/sympy/logic/algorithms/dpll.py +++ b/sympy/logic/algorithms/dpll.py @@ -8,11 +8,13 @@ - http://bioinformatics.louisville.edu/ouyang/MingOuyangThesis.pdf """ from sympy.core import Symbol -from sympy.logic.boolalg import Or, Not, conjuncts, disjuncts, to_cnf +from sympy.logic.boolalg import Or, Not, conjuncts, disjuncts, to_cnf, \ + to_int_repr from sympy.logic.inference import pl_true, literal_symbol def dpll_satisfiable(expr): - """Check satisfiability of a propositional sentence. + """ + Check satisfiability of a propositional sentence. It returns a model rather than True when it succeeds >>> from sympy import symbols >>> A, B = symbols('AB') @@ -21,9 +23,16 @@ def dpll_satisfiable(expr): >>> dpll_satisfiable(A & ~A) False """ - clauses = conjuncts(to_cnf(expr)) symbols = list(expr.atoms(Symbol)) - return dpll(clauses, symbols, {}) + symbols_int_repr = range(1, len(symbols) + 1) + clauses = conjuncts(to_cnf(expr)) + clauses_int_repr = to_int_repr(clauses, symbols) + result = dpll_int_repr(clauses_int_repr, symbols_int_repr, {}) + if not result: return result + output = {} + for key in result: + output.update({symbols[key-1]: result[key]}) + return output def dpll(clauses, symbols, model): """Compute satisfiability in a partial model""" @@ -62,11 +71,72 @@ def dpll(clauses, symbols, model): return (dpll(clauses, symbols, model) or dpll(clauses, symbols_copy, model_copy)) +def dpll_int_repr(clauses, symbols, model): + """ + Compute satisfiability in a partial model. + Arguments are expected to be in integer representation + """ + # compute DP kernel + P, value = find_unit_clause_int_repr(clauses, model) + while P: + model.update({P: value}) + symbols.remove(P) + if not value: P = -P + clauses = unit_propagate_int_repr(clauses, P) + P, value = find_unit_clause_int_repr(clauses, model) + P, value = find_pure_symbol_int_repr(symbols, clauses) + while P: + model.update({P: value}) + symbols.remove(P) + if not value: P = -P + clauses = unit_propagate_int_repr(clauses, P) + P, value = find_pure_symbol_int_repr(symbols, clauses) + # end DP kernel + unknown_clauses = [] + for c in clauses: + val = pl_true_int_repr(c, model) + if val == False: + return False + if val != True: + unknown_clauses.append(c) + if not unknown_clauses: + return model + if not clauses: return model + P = symbols.pop() + model_copy = model.copy() + model.update({P: True}) + model_copy.update({P: False}) + symbols_copy = symbols[:] + return (dpll_int_repr(clauses, symbols, model) or + dpll_int_repr(clauses, symbols_copy, model_copy)) + ### helper methods for DPLL +def pl_true_int_repr(clause, model={}): + """ + Lightweith version of pl_true. + Expects its arguments are written in CNF form and integer representation + """ + if len(clause) == 1: + c = clause[0] + if c in model: return model.get(c) + if -c in model: return not model.get(-c) + return None + result = False + for l in clause: + p = pl_true_int_repr([l], model) + if p: return True + if p is None: result = None + return result + def unit_propagate(clauses, symbol): - """Returns an equivalent set of clauses - http://en.wikipedia.org/wiki/Unit_propagation + """ + Returns an equivalent set of clauses + If a set of clauses contains the unit clause l, the other clauses are + simplified by the application of the two following rules: + + 1. every clause containing l is removed + 2. in every clause that contains ~l this literal is deleted """ output = [] for c in clauses: @@ -83,8 +153,27 @@ def unit_propagate(clauses, symbol): output.append(c) return output +def unit_propagate_int_repr(clauses, symbol): + """ + Same as above, but arguments are expected to be in integer + representation + """ + output = [] + for c in clauses: + if len(c) == 1: + output.append(c) + continue + for l in c: + if l == symbol: break + elif l == -symbol: + output.append([x for x in c if x != l]) + break + else: output.append(c) + return output + def find_pure_symbol(symbols, unknown_clauses): - """Find a symbol and its value if it appears only as a positive literal + """ + Find a symbol and its value if it appears only as a positive literal (or only as a negative) in clauses. >>> from sympy import symbols >>> A, B, C = symbols('ABC') @@ -99,8 +188,25 @@ def find_pure_symbol(symbols, unknown_clauses): if found_pos != found_neg: return sym, found_pos return None, None +def find_pure_symbol_int_repr(symbols, unknown_clauses): + """ + Same as find_pure_symbol, but arguments are expected + to be in integer representation + + >>> find_pure_symbol_int_repr([1,2,3], [[1, -2], [-2, -3], [3, 1]]) + (1, True) + """ + for sym in symbols: + found_pos, found_neg = False, False + for c in unknown_clauses: + if not found_pos and sym in c: found_pos = True + if not found_neg and -sym in c: found_neg = True + if found_pos ^ found_neg: return sym, found_pos + return None, None + def find_unit_clause(clauses, model): - """A unit clause has only 1 variable that is not bound in the model. + """ + A unit clause has only 1 variable that is not bound in the model. >>> from sympy import symbols >>> A, B, C = symbols('ABC') >>> find_unit_clause([A | B | C, B | ~C, A | ~B], {A:True}) @@ -116,3 +222,22 @@ def find_unit_clause(clauses, model): if num_not_in_model == 1: return P, value return None, None + +def find_unit_clause_int_repr(clauses, model): + """ + Same as find_unit_clause, but arguments are expected to be in + integer representation + """ + for c in clauses: + num_not_in_model = False + for literal in c: + sym = abs(literal) + if sym not in model: + if num_not_in_model: + num_not_in_model = False + break + num_not_in_model = True + P, value = sym, literal > 0 + if num_not_in_model: + return P, value + return None, None diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py index 95a3a4b..dfc9ed2 100755 --- a/sympy/logic/boolalg.py +++ b/sympy/logic/boolalg.py @@ -174,7 +174,8 @@ def disjuncts(expr): return [expr] def distribute_and_over_or(expr): - """Given a sentence s consisting of conjunctions and disjunctions + """ + Given a sentence s consisting of conjunctions and disjunctions of literals, return an equivalent sentence in CNF. """ if isinstance(expr, Or): @@ -194,6 +195,13 @@ def distribute_and_over_or(expr): def to_cnf(expr): """Convert a propositional logical sentence s to conjunctive normal form. That is, of the form ((A | ~B | ...) & (B | C | ...) & ...) + + Examples: + + >>> from sympy import symbols + >>> A, B, C = symbols('A B C') + >>> to_cnf(~(A | B) | C) + And(Or(C, Not(A)), Or(C, Not(B))) """ expr = sympify(expr) expr = eliminate_implications(expr) @@ -224,3 +232,29 @@ def compile_rule(s): """ import re return eval(re.sub(r'([a-zA-Z0-9_.]+)', r'Symbol("\1")', s), {'Symbol' : Symbol}) + + +def to_int_repr(clauses, symbols): + """ + takes clauses in CNF puts them into integer representation + + Examples: + >>> from sympy import symbols + >>> x, y = symbols('x y') + >>> to_int_repr([x | y, y], [x, y]) + [[1, 2], [2]] + """ + def append_symbol(arg, symbols): + if type(arg) is Not: return -(symbols.index(arg.args[0])+1) + else: return symbols.index(arg)+1 + + output = [] + for c in clauses: + if type(c) is Or: + t = [] + for arg in c.args: + t.append(append_symbol(arg, symbols)) + output.append(t) + else: + output.append([append_symbol(c, symbols)]) + return output diff --git a/sympy/logic/inference.py b/sympy/logic/inference.py index 59531bb..5534593 100755 --- a/sympy/logic/inference.py +++ b/sympy/logic/inference.py @@ -58,11 +58,11 @@ def pl_true(expr, model={}): return model.get(expr) args = expr.args - if isinstance(expr, Not): + if type(expr) is Not: p = pl_true(args[0], model) if p is None: return None else: return not p - elif isinstance(expr, Or): + elif type(expr) is Or: result = False for arg in args: p = pl_true(arg, model) diff --git a/sympy/logic/tests/test_boolalg.py b/sympy/logic/tests/test_boolalg.py index 478dee3..05d8397 100755 --- a/sympy/logic/tests/test_boolalg.py +++ b/sympy/logic/tests/test_boolalg.py @@ -1,6 +1,6 @@ -from sympy.logic.boolalg import And, Or, Xor, Not, Nand, Nor, Implies, Equivalent, to_cnf, \ - eliminate_implications, distribute_and_over_or, compile_rule, conjuncts, \ - disjuncts +from sympy.logic.boolalg import And, Or, Xor, Not, Nand, Nor, Implies, \ + Equivalent, to_cnf, eliminate_implications, distribute_and_over_or, \ + compile_rule, conjuncts, disjuncts, to_int_repr from sympy import symbols from sympy.utilities.pytest import raises, XFAIL @@ -194,3 +194,9 @@ def test_to_cnf(): def test_compile_rule(): from sympy import sympify assert compile_rule("A & B") == sympify("A & B") + +def test_to_int_repr(): + x, y, z = symbols('x y z') + assert to_int_repr([x | y, z | x], [x, y, z]) == [[1, 2], [1, 3]] + assert to_int_repr([x | y, z | ~x], [x, y, z]) == [[1, 2], [3, -1]] + diff --git a/sympy/logic/tests/test_inference.py b/sympy/logic/tests/test_inference.py index b3eaad8..9cd84ba 100755 --- a/sympy/logic/tests/test_inference.py +++ b/sympy/logic/tests/test_inference.py @@ -3,9 +3,11 @@ from sympy import symbols from sympy.logic.boolalg import Equivalent, Implies from sympy.logic.inference import pl_true, satisfiable, PropKB -from sympy.logic.algorithms.dpll import dpll, dpll_satisfiable, find_pure_symbol, \ - find_unit_clause, unit_propagate -from sympy.utilities.pytest import raises +from sympy.logic.algorithms.dpll import dpll, dpll_satisfiable, \ + find_pure_symbol, find_unit_clause, unit_propagate, \ + find_pure_symbol_int_repr, find_unit_clause_int_repr, \ + unit_propagate_int_repr +from sympy.utilities.pytest import raises, XFAIL def test_find_pure_symbol(): A, B, C = symbols('ABC') @@ -16,26 +18,55 @@ def test_find_pure_symbol(): assert find_pure_symbol([A, B, C], [~A | ~B, ~B | ~C, C | A]) == (B, False) assert find_pure_symbol([A, B, C], [~A | B, ~B | ~C, C | A]) == (None, None) +def test_find_pure_symbol_int_repr(): + assert find_pure_symbol_int_repr([1], [[1]]) == (1, True) + assert find_pure_symbol_int_repr([1, 2], [[-1, 2], [-2, 1]]) == (None, None) + assert find_pure_symbol_int_repr([1, 2, 3], [[1, -2], [-2, -3], [3, 1]]) == \ + (1, True) + assert find_pure_symbol_int_repr([1, 2, 3], [[-1, 2], [2, -3], [3, 1]]) == \ + (2, True) + assert find_pure_symbol_int_repr([1, 2, 3], [[-1, -2], [-2, -3], [3, 1]]) == \ + (2, False) + assert find_pure_symbol_int_repr([1, 2, 3], [[-1, 2], [-2, -3], [3, 1]]) == \ + (None, None) + def test_unit_clause(): A, B, C = symbols('ABC') assert find_unit_clause([A], {}) == (A, True) - assert find_unit_clause([A, ~A], {}) == (A, True) + assert find_unit_clause([A, ~A], {}) == (A, True) ### Wrong ?? assert find_unit_clause([A | B], {A: True}) == (B, True) assert find_unit_clause([A | B], {B: True}) == (A, True) assert find_unit_clause([A | B | C, B | ~C, A | ~B], {A:True}) == (B, False) assert find_unit_clause([A | B | C, B | ~C, A | B], {A:True}) == (B, True) assert find_unit_clause([A | B | C, B | ~C, A ], {}) == (A, True) +def test_unit_clause_int_repr(): + assert find_unit_clause_int_repr([[1]], {}) == (1, True) + assert find_unit_clause_int_repr([[1], [-1]], {}) == (1, True) + assert find_unit_clause_int_repr([[1,2]], {1: True}) == (2, True) + assert find_unit_clause_int_repr([[1,2]], {2: True}) == (1, True) + assert find_unit_clause_int_repr([[1,2,3], [2, -3], [1, -2]], {1: True}) == \ + (2, False) + assert find_unit_clause_int_repr([[1, 2, 3], [3, -3], [1, 2]], {1: True}) == \ + (2, True) +# assert find_unit_clause([A | B | C, B | ~C, A ], {}) == (A, True) + def test_unit_propagate(): A, B, C = symbols('ABC') assert unit_propagate([A | B], A) == [] assert unit_propagate([A | B, ~A | C, ~C | B, A], A) == [C, ~C | B, A] +def test_unit_propagate_int_repr(): + assert unit_propagate_int_repr([[1, 2]], 1) == [] + assert unit_propagate_int_repr([[1, 2], [-1, 3], [-3, 2], [1]], 1) == \ + [[3], [-3, 2], [1]] + def test_dpll(): """This is also tested in test_dimacs""" A, B, C = symbols('ABC') assert dpll([A | B], [A, B], {A: True, B: True}) == {A: True, B: True} +...@xfail # We need to reconvert the output of dpll def test_dpll_satisfiable(): A, B, C = symbols('ABC') assert dpll_satisfiable( A & ~A ) == False -- 1.6.4 --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "sympy-patches" group. To post to this group, send email to sympy-patches@googlegroups.com To unsubscribe from this group, send email to sympy-patches+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/sympy-patches?hl=en -~----------~----~----~----~------~----~------~--~---
