This is a replacement for sympy.core.logic and will be used extensively by the query module. The old logic module can be removed once the old assumption system is removed.
Contents -------- sympy.logic.boolalg - Operators for boolean algebra on symbols {And: &, Or: |, Not: ~} - some useful methods, mainly used to convert expressions to conjunctive normal form (CNF) sympy.logic.inference - Rules for inference in propositional logic. Main method here is satisfiable(expr), which checks satisfiability of a propositional sentence (for now using dpll algorithm) sympy.logic.kb - Definition of a knowledge base sympy.algorithms - some algorithms used by higher order methods (just DPLL for now), but in a future we should also have Quine-McCluskey for simplification of boolean expressions Most of the methods in this module are implementations of algorithms described in the book "AI: A modern approach", http://aima.cs.berkeley.edu/ --- sympy/core/basic.py | 26 ++++++- sympy/logic/__init__.py | 2 + sympy/logic/algorithms/dpll.py | 49 +++++++++++ sympy/logic/boolalg.py | 155 +++++++++++++++++++++++++++++++++++ sympy/logic/inference.py | 119 +++++++++++++++++++++++++++ sympy/logic/kb.py | 36 ++++++++ sympy/logic/tests/test_boolalg.py | 110 +++++++++++++++++++++++++ sympy/logic/tests/test_inference.py | 46 ++++++++++ 8 files changed, 541 insertions(+), 2 deletions(-) create mode 100644 sympy/logic/__init__.py create mode 100644 sympy/logic/algorithms/__init__.py create mode 100644 sympy/logic/algorithms/dpll.py create mode 100755 sympy/logic/boolalg.py create mode 100755 sympy/logic/inference.py create mode 100644 sympy/logic/kb.py create mode 100755 sympy/logic/tests/test_boolalg.py create mode 100755 sympy/logic/tests/test_inference.py diff --git a/sympy/core/basic.py b/sympy/core/basic.py index b48e633..6ab3101 100644 --- a/sympy/core/basic.py +++ b/sympy/core/basic.py @@ -680,8 +680,30 @@ def __rdiv__(self, other): __truediv__ = __div__ __rtruediv__ = __rdiv__ - - + # ******************* + # * Logic operators * + # ******************* + + def __and__(self, other): + """Overloading for & operator""" + from sympy.logic.boolalg import And + return And(self, other) + def __or__(self, other): + """Overloading for |""" + from sympy.logic.boolalg import Or + return Or(self, other) + def __invert__(self): + """Overloading for ~""" + from sympy.logic.boolalg import Not + return Not(self) + def __rshift__(self, other): + """Overloading for >>""" + from sympy.logic.boolalg import Implies + return Implies(self, other) + def __lshift__(self, other): + """Overloading for <<""" + from sympy.logic.boolalg import Implies + return Implies(other, self) def __repr__(self): diff --git a/sympy/logic/__init__.py b/sympy/logic/__init__.py new file mode 100644 index 0000000..5076249 --- /dev/null +++ b/sympy/logic/__init__.py @@ -0,0 +1,2 @@ +from boolalg import * +from inference import * \ No newline at end of file diff --git a/sympy/logic/algorithms/__init__.py b/sympy/logic/algorithms/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/sympy/logic/algorithms/dpll.py b/sympy/logic/algorithms/dpll.py new file mode 100644 index 0000000..77d92ed --- /dev/null +++ b/sympy/logic/algorithms/dpll.py @@ -0,0 +1,49 @@ +from sympy.core import Symbol +from sympy.logic.boolalg import conjuncts, to_cnf +from sympy.logic.inference import find_pure_symbol, find_unit_clause, pl_true + +def dpll_satisfiable(expr): + """Check satisfiability of a propositional sentence. + It returns a model rather than True when it succeeds + >>> from sympy import symbols + >>> A, B = symbols('AB') + >>> dpll_satisfiable(A & ~B) + {A: True, B: False} + >>> dpll_satisfiable(A & ~A) + False + + References: Implemented as described in http://aima.cs.berkeley.edu/ + """ + clauses = conjuncts(to_cnf(expr)) + symbols = list(expr.atoms(Symbol)) + return dpll(clauses, symbols, {}) + +def dpll(clauses, symbols, model): + """See if the clauses are true in a partial model. + http://en.wikipedia.org/wiki/DPLL_algorithm + """ + unknown_clauses = [] ## clauses with an unknown truth value + for c in clauses: + val = pl_true(c, model) + if val == False: + return False + if val != True: + unknown_clauses.append(c) + if not unknown_clauses: + return model + P, value = find_pure_symbol(symbols, unknown_clauses) + if P: + model.update({P: value}) + syms = [x for x in symbols if x != P] + return dpll(clauses, syms, model) + P, value = find_unit_clause(clauses, model) + if P: + model.update({P: value}) + syms = [x for x in symbols if x != P] + return dpll(clauses, syms, model) + P = symbols.pop() + model_1, model_2 = model.copy(), model.copy() + model_1.update({P: True}) + model_2.update({P: False}) + return (dpll(clauses, symbols, model_1) or + dpll(clauses, symbols, model_2)) \ No newline at end of file diff --git a/sympy/logic/boolalg.py b/sympy/logic/boolalg.py new file mode 100755 index 0000000..1a57740 --- /dev/null +++ b/sympy/logic/boolalg.py @@ -0,0 +1,155 @@ +"""Boolean algebra module for SymPy""" +from sympy.core import Basic, Function, sympify, Symbol +from sympy.utilities import flatten + + +class BooleanFunction(Function): + """Boolean function is a function that lives in a boolean space + It is used as base class for And, Or, Not, etc. + """ + pass + +class And(BooleanFunction): + """Evaluates to True if all it's arguments are True, + False otherwise""" + @classmethod + def eval(cls, *args): + if len(args) < 2: raise ValueError("And must have at least two arguments") + out_args = [] + for i, arg in enumerate(args): # we iterate over a copy or args + if isinstance(arg, bool): + if not arg: return False + else: continue + out_args.append(arg) + if len(out_args) == 0: return True + if len(out_args) == 1: return out_args[0] + sargs = sorted(flatten(out_args, cls=cls)) + return Basic.__new__(cls, *sargs) + +class Or(BooleanFunction): + @classmethod + def eval(cls, *args): + if len(args) < 2: raise ValueError("And must have at least two arguments") + out_args = [] + for i, arg in enumerate(args): # we iterate over a copy or args + if isinstance(arg, bool): + if arg: return True + else: continue + out_args.append(arg) + if len(out_args) == 0: return False + if len(out_args) == 1: return out_args[0] + sargs = sorted(flatten(out_args, cls=cls)) + return Basic.__new__(cls, *sargs) + +class Not(BooleanFunction): + """De Morgan rules applied automatically, so Not is moved inward""" + @classmethod + def eval(cls, *args): + if len(args) > 1: + return map(cls, args) + arg = args[0] + # apply De Morgan Rules + if isinstance(arg, And): + return Or( *[Not(a) for a in arg.args]) + if isinstance(arg, Or): + return And(*[Not(a) for a in arg.args]) + if isinstance(arg, bool): return not arg + if isinstance(arg, Not): + if len(arg.args) == 1: return arg.args[0] + return arg.args + +class Implies(BooleanFunction): + def __init__(self, *args, **kwargs): + if len(args) != 2: raise ValueError("Wrong set of arguments") + return super(BooleanFunction, self).__init__(*args, **kwargs) + +class Equivalent(BooleanFunction): + pass + +### end class definitions. Some useful methods + +def conjuncts(expr): + """Return a list of the conjuncts in the expr s. + >>> from sympy import symbols + >>> A, B = symbols('AB') + >>> conjuncts(A & B) + [A, B] + >>> conjuncts(A | B) + [Or(A, B)] + """ + if isinstance(expr, And): + return list(expr.args) + else: + return [expr] + +def disjuncts(expr): + """Return a list of the disjuncts in the sentence s. + >>> from sympy import symbols + >>> A, B = symbols('AB') + >>> disjuncts(A | B) + [A, B] + >>> disjuncts(A & B) + [And(A, B)] + """ + if isinstance(expr, Or): + return list(expr.args) + else: + return [expr] + +def distribute_and_over_or(expr): + """Given a sentence s consisting of conjunctions and disjunctions + of literals, return an equivalent sentence in CNF. + """ + if isinstance(expr, Or): + expr = Or(*expr.args) + if len(expr.args) == 0: + return False + if len(expr.args) == 1: + return distribute_and_over_or(expr.args[0]) + for arg in expr.args: + if isinstance(arg, And): + conj = arg + break + else: return type(expr)(*expr.args) + others = [a for a in expr.args if a is not conj] + if len(others) == 1: + rest = others[0] + else: + rest = Or(*others) + return And(*map(distribute_and_over_or, + [Or(c, rest) for c in conj.args])) + elif isinstance(expr, And): + return And(*map(distribute_and_over_or, expr.args)) + else: + return expr + +def to_cnf(expr): + """Convert a propositional logical sentence s to conjunctive normal form. + That is, of the form ((A | ~B | ...) & (B | C | ...) & ...) + """ + expr = sympify(expr) + expr = eliminate_implications(expr) + return distribute_and_over_or(expr) + +def eliminate_implications(expr): + """Change >>, <<, and <=> into &, |, and ~. That is, return an Expr + that is equivalent to s, but has only &, |, and ~ as logical operators. + """ + expr = sympify(expr) + if expr.is_Atom: return expr ## (Atoms are unchanged.) + args = map(eliminate_implications, expr.args) + a, b = args[0], args[-1] # TODO: multiple implications? + if isinstance(expr, Implies): + return Or(b, Not(a)) + elif isinstance(expr, Equivalent): + return And(Or(a, Not(b)), Or(b, Not(a))) + else: + return type(expr)(*args) + +def compile_rule(s): + """Transforms a rule into a sympy expression + A rule is a string of the form "symbol1 & symbol2 | ..." + See sympy.assumptions.known_facts for examples of rules + """ + import re + return eval(re.sub(r'([a-zA-Z0-9_.]+)', r'Symbol("\1")', s), {'Symbol' : Symbol}) \ No newline at end of file diff --git a/sympy/logic/inference.py b/sympy/logic/inference.py new file mode 100755 index 0000000..a638ee2 --- /dev/null +++ b/sympy/logic/inference.py @@ -0,0 +1,119 @@ +"""Inference in propositional logic""" +from sympy.core import Symbol +from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent, disjuncts, \ + to_cnf + + +def find_pure_symbol(symbols, unknown_clauses): + """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') + >>> find_pure_symbol([A, B, C], [A|~B,~B|~C,C|A]) + (A, True) + """ + for sym in symbols: + found_pos, found_neg = False, False + for c in unknown_clauses: + if not found_pos and sym in disjuncts(c): found_pos = True + if not found_neg and Not(sym) in disjuncts(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. + >>> from sympy import symbols + >>> A, B, C = symbols('ABC') + >>> find_unit_clause([A | B | C, B | ~C, A | ~B], {A:True}) + (B, True) + """ + for clause in clauses: + num_not_in_model = 0 + for literal in disjuncts(clause): + sym = literal_symbol(literal) + if sym not in model: + num_not_in_model += 1 + P, value = sym, (isinstance(literal, Not)) + if num_not_in_model == 1: + return P, value + return None, None + +def literal_symbol(literal): + """The symbol in this literal (without the negation). + >>> from sympy import Symbol + >>> A = Symbol('A') + >>> literal_symbol(A) + A + >>> literal_symbol(~A) + A + """ + if isinstance(literal, Not): + return literal.args[0] + else: + return literal + +def satisfiable(expr, algorithm="dpll"): + """Check satisfiability of a propositional sentence. + Returns a model when it succeeds + + Examples + >>> from sympy import symbols + >>> A, B = symbols('AB') + >>> satisfiable(A & ~B) + {A: True, B: False} + >>> satisfiable(A & ~A) + False + """ + expr = to_cnf(expr) + if algorithm == "dpll": + from sympy.logic.algorithms.dpll import dpll_satisfiable + return dpll_satisfiable(expr) + raise NotImplementedError + +def pl_true(expr, model={}): + """Return True if the propositional logic expression is true in the model, + and False if it is false. If the model does not specify the value for + every proposition, this may return None to indicate 'not obvious'; + this may happen even when the expression is tautological. + + The model is implemented as a dict containing the pair symbol, boolean value. + + Examples: + >>> from sympy import symbols + >>> A, B = symbols('AB') + >>> pl_true( A & B, {A: True, B : True}) + True + """ + args = expr.args + if isinstance(expr, bool): + return expr + if expr.is_Atom: return model.get(expr) + elif isinstance(expr, Not): + p = pl_true(args[0], model) + if p is None: return None + else: return not p + elif isinstance(expr, Or): + result = False + for arg in args: + p = pl_true(arg, model) + if p == True: return True + if p == None: result = None + return result + elif isinstance(expr, And): + result = True + for arg in args: + p = pl_true(arg, model) + if p == False: return False + if p == None: result = None + return result + p, q = args + if isinstance(expr, Implies): + return pl_true(Or(Not(p), q), model) + pt = pl_true(p, model) + if pt == None: return None + qt = pl_true(q, model) + if qt == None: return None + if isinstance(expr, Equivalent): + return pt == qt + else: + raise ValueError, "Illegal operator in logic expression" + str(exp) \ No newline at end of file diff --git a/sympy/logic/kb.py b/sympy/logic/kb.py new file mode 100644 index 0000000..267af91 --- /dev/null +++ b/sympy/logic/kb.py @@ -0,0 +1,36 @@ +from sympy.logic.boolalg import And, conjuncts, to_cnf +from sympy.logic.inference import satisfiable + +class KB(object): + pass + +class PropKB(KB): + "A KB for Propositional Logic. Inefficient, with no indexing." + + def __init__(self, sentence=None): + self.clauses = [] + if sentence: + self.tell(sentence) + + def tell(self, sentence): + "Add the sentence's clauses to the KB" + self.clauses.extend(conjuncts(to_cnf(sentence))) + + def ask(self, query): + """TODO: examples""" + if len(self.clauses) == 0: return {} + query_conjuncts = conjuncts(to_cnf(~query)) + query_conjuncts.extend(self.clauses) + return not satisfiable(And(*query_conjuncts)) + + def ask_generator(self, query): + "Yield the empty substitution if KB implies query; else False" + if not tt_entails(Expr('&', *self.clauses), query): + return + yield {} + + def retract(self, sentence): + "Remove the sentence's clauses from the KB" + for c in conjuncts(to_cnf(sentence)): + if c in self.clauses: + self.clauses.remove(c) \ No newline at end of file diff --git a/sympy/logic/tests/test_boolalg.py b/sympy/logic/tests/test_boolalg.py new file mode 100755 index 0000000..e4f1c32 --- /dev/null +++ b/sympy/logic/tests/test_boolalg.py @@ -0,0 +1,110 @@ +from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent, to_cnf, \ + eliminate_implications, distribute_and_over_or +from sympy import symbols +from sympy.utilities.pytest import raises + +def test_overloading(): + """Test that |, & are overloaded as expected""" + A, B, C = symbols('ABC') + assert A & B == And(A, B) + assert A | B == Or(A, B) + assert (A & B) | C == Or(And(A, B), C) + assert A >> B == Implies(A, B) + assert A << B == Implies(B, A) + assert ~A == Not(A) + +def test_bool_unary(): + """Test boolean functions with one argument + Only Not is well defined in this case. + All other functions should raise a ValueError + """ + A = symbols('A') + assert Not(True ) == False + assert Not(False) == True + raises(ValueError, "And(True)") + raises(ValueError, "And(False)") + raises(ValueError, "And(A)") + raises(ValueError, "Or(True)") + raises(ValueError, "Or(False)") + raises(ValueError, "Or(A)") + +def test_And_bool_2(): + """Test And with two boolean arguments""" + assert And(True, True ) == True + assert And(True, False) == False + assert And(False, False) == False + +def test_Or_bool(): + assert Or(True, True ) == True + assert Or(True, False) == True + assert Or(False, False) == False + +def test_Not_bool(): + assert Not(True, True ) == [False, False] + assert Not(True, False) == [False, True ] + assert Not(False,False) == [True, True ] + +def test_Implies(): + A, B, C = symbols('ABC') + raises(ValueError, "Implies()") + raises(ValueError, "Implies(A)") + raises(ValueError, "Implies(A, B, C)") + +def test_bool_symbol(): + """Test that mixing symbols with boolean values + works as expected""" + A, B, C = symbols('ABC') + assert And(A, True) == A + assert And(A, True, True) == A + assert And(A, False) == False + assert And(A, True, False) == False + assert Or(A, True) == True + assert Or(A, False) == A + +""" +we test for axioms of boolean algebra +see http://en.wikipedia.org/wiki/Boolean_algebra_(structure) +""" + +def test_commutative(): + """Test for commutativity of And and Not""" + A, B = symbols('AB') + assert A & B == B & A + assert A | B == B | A + +def test_and_associativity(): + """Test for associativity of And""" + A, B, C = symbols('ABC') + assert (A & B) & C == A & (B & C) + +def test_or_assicativity(): + A, B, C = symbols('ABC') + assert ((A | B) | C) == (A | (B | C)) + +def test_double_negation(): + a = symbols('a') + assert ~(~a) == a + +def test_De_Morgan(): + A, B = symbols('AB') + assert ~(A & B) == (~A) | (~B) + assert ~(A | B) == (~A) & (~B) + + +# test methods +def test_eliminate_implications(): + A, B, C = symbols('ABC') + assert eliminate_implications( A >> B) == (~A) | B + assert eliminate_implications(A >> (C >>Not(B))) \ + == Or(Or(Not(B), Not(C)), Not(A)) + +def test_distribute(): + A, B, C = symbols('ABC') + assert distribute_and_over_or(Or(And(A, B), C)) == And(Or(A, C), Or(B, C)) + + +def test_to_cnf(): + A, B, C = symbols('ABC') + assert to_cnf(Not(Or(B, C))) == And(Not(B), Not(C)) + assert to_cnf(Equivalent(A, Or(B,C))) == \ + And(Or(Not(B), A), Or(Not(C), A), Or(B, C, Not(A))) diff --git a/sympy/logic/tests/test_inference.py b/sympy/logic/tests/test_inference.py new file mode 100755 index 0000000..6667e15 --- /dev/null +++ b/sympy/logic/tests/test_inference.py @@ -0,0 +1,46 @@ +from sympy import symbols +from sympy.logic.boolalg import And, Not, Or, Equivalent, Implies, to_cnf +from sympy.logic.inference import pl_true, satisfiable +from sympy.logic.algorithms.dpll import dpll +from sympy.logic.kb import PropKB + + +def test_satisfiable(): + A, B, C = symbols('ABC') + assert satisfiable( A & ~A ) == False + assert satisfiable( A & ~B ) == {A: True, B: False} + assert satisfiable( A & B & C ) == {A: True, B: True, C: True} + assert satisfiable( A | B ) in ({A: True}, {B: True}) + +def test_satisfiable_1(): + """We prove expr entails alpha proving expr & ~B is unsatisfiable""" + A, B, C = symbols('ABC') + assert satisfiable(A & (A >> B) & ~B) == False + +def test_pl_true(): + A, B, C = symbols('ABC') + assert pl_true( And(A, B), {A : True, B : True}) == True + assert pl_true( Or(A, B), {A : True}) == True + assert pl_true( Or(A, B), {B : True}) == True + + # test for false + assert pl_true ( And(A, B), {A: False, B: False}) == False + assert pl_true ( And(A, B), {A: False}) == False + assert pl_true ( And(A, B), {B: False}) == False + assert pl_true ( Or(A, B), {A: False, B: False}) == False + +def test_PropKB(): + A, B, C = symbols('ABC') + kb = PropKB() + kb.tell(A) + kb.tell(A >> B) + kb.tell(B >> C) + assert kb.ask(B) == True + assert kb.ask(C) == True + "TODO: test for api: .clauses etc" + +def test_propKB_tolerant(): + """"Test that it is tolerant to bad input""" + kb = PropKB() + A, B, C = symbols('ABC') + assert kb.ask(B) == {} -- 1.6.1.2 --~--~---------~--~----~------------~-------~--~----~ 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 -~----------~----~----~----~------~----~------~--~---