modelparameters.sympy.logic package

Subpackages

• modelparameters.sympy.logic.algorithms package
  • Submodules
  • modelparameters.sympy.logic.algorithms.dpll module
    • dpll()
    • dpll_int_repr()
    • dpll_satisfiable()
    • find_pure_symbol()
    • find_pure_symbol_int_repr()
    • find_unit_clause()
    • find_unit_clause_int_repr()
    • pl_true_int_repr()
    • unit_propagate()
    • unit_propagate_int_repr()
  • modelparameters.sympy.logic.algorithms.dpll2 module
    • Level
    • SATSolver
    • dpll_satisfiable()
  • Module contents
• modelparameters.sympy.logic.utilities package
  • Submodules
  • modelparameters.sympy.logic.utilities.dimacs module
    • load()
    • load_file()
  • Module contents

Submodules

modelparameters.sympy.logic.boolalg module

Boolean algebra module for SymPy

class modelparameters.sympy.logic.boolalg.And(*args)

Bases: LatticeOp, BooleanFunction

Logical AND function.

It evaluates its arguments in order, giving False immediately if any of them are False, and True if they are all True.

Examples

>>> from ..core import symbols
>>> from ..abc import x, y
>>> from .boolalg import And
>>> x & y
x & y

Notes

The & operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise and. Hence, And(a, b) and a & b will return different things if a and b are integers.

>>> And(x, y).subs(x, 1)
y

as_set()

Rewrite logic operators and relationals in terms of real sets.

Examples

>>> from .. import And, Symbol
>>> x = Symbol('x', real=True)
>>> And(x<2, x>-2).as_set()
Interval.open(-2, 2)

default_assumptions = {'commutative': True}

identity = True

is_commutative

nargs = S.Naturals0

zero = False

class modelparameters.sympy.logic.boolalg.Boolean(*args)

Bases: Basic

A boolean object is an object for which logic operations make sense.

default_assumptions = {}

equals(other)

Returns True if the given formulas have the same truth table. For two formulas to be equal they must have the same literals.

Examples

>>> from ..abc import A, B, C
>>> from .boolalg import And, Or, Not
>>> (A >> B).equals(~B >> ~A)
True
>>> Not(And(A, B, C)).equals(And(Not(A), Not(B), Not(C)))
False
>>> Not(And(A, Not(A))).equals(Or(B, Not(B)))
False

class modelparameters.sympy.logic.boolalg.BooleanAtom(*args)

Bases: Boolean

Base class of BooleanTrue and BooleanFalse.

property canonical

default_assumptions = {}

expand(*a, **kw)

is_Atom = True

is_Boolean = True

simplify(*a, **kw)

class modelparameters.sympy.logic.boolalg.BooleanFalse(*args, **kwargs)

Bases: BooleanAtom

SymPy version of False, a singleton that can be accessed via S.false.

This is the SymPy version of False, for use in the logic module. The primary advantage of using false instead of False is that shorthand boolean operations like ~ and >> will work as expected on this class, whereas with False they act bitwise on 0. Functions in the logic module will return this class when they evaluate to false.

Notes

See note in :py:class`sympy.logic.boolalg.BooleanTrue`

Examples

>>> from .. import sympify, false, Or, true
>>> sympify(False)
False
>>> false >> false
True
>>> False >> False
0
>>> Or(True, False)
True

See also

sympy.logic.boolalg.BooleanTrue

as_set()

Rewrite logic operators and relationals in terms of real sets.

Examples

>>> from .. import false
>>> false.as_set()
EmptySet()

default_assumptions = {}

class modelparameters.sympy.logic.boolalg.BooleanFunction(*args)

Bases: Application, Boolean

Boolean function is a function that lives in a boolean space It is used as base class for And, Or, Not, etc.

default_assumptions = {}

is_Boolean = True

to_nnf(simplify=True)

class modelparameters.sympy.logic.boolalg.BooleanTrue(*args, **kwargs)

Bases: BooleanAtom

SymPy version of True, a singleton that can be accessed via S.true.

This is the SymPy version of True, for use in the logic module. The primary advantage of using true instead of True is that shorthand boolean operations like ~ and >> will work as expected on this class, whereas with True they act bitwise on 1. Functions in the logic module will return this class when they evaluate to true.

Notes

There is liable to be some confusion as to when True should be used and when S.true should be used in various contexts throughout SymPy. An important thing to remember is that sympify(True) returns S.true. This means that for the most part, you can just use True and it will automatically be converted to S.true when necessary, similar to how you can generally use 1 instead of S.One.

The rule of thumb is:

“If the boolean in question can be replaced by an arbitrary symbolic Boolean, like Or(x, y) or x > 1, use S.true. Otherwise, use True”

In other words, use S.true only on those contexts where the boolean is being used as a symbolic representation of truth. For example, if the object ends up in the .args of any expression, then it must necessarily be S.true instead of True, as elements of .args must be Basic. On the other hand, == is not a symbolic operation in SymPy, since it always returns True or False, and does so in terms of structural equality rather than mathematical, so it should return True. The assumptions system should use True and False. Aside from not satisfying the above rule of thumb, the assumptions system uses a three-valued logic (True, False, None), whereas S.true and S.false represent a two-valued logic. When in doubt, use True.

“S.true == True is True.”

While “S.true is True” is False, “S.true == True” is True, so if there is any doubt over whether a function or expression will return S.true or True, just use == instead of is to do the comparison, and it will work in either case. Finally, for boolean flags, it’s better to just use if x instead of if x is True. To quote PEP 8:

Don’t compare boolean values to True or False using ==.

• Yes: if greeting:

• No: if greeting == True:

• Worse: if greeting is True:

Examples

>>> from .. import sympify, true, Or
>>> sympify(True)
True
>>> ~true
False
>>> ~True
-2
>>> Or(True, False)
True

See also

sympy.logic.boolalg.BooleanFalse

as_set()

Rewrite logic operators and relationals in terms of real sets.

Examples

>>> from .. import true
>>> true.as_set()
UniversalSet()

default_assumptions = {}

class modelparameters.sympy.logic.boolalg.Equivalent(*args)

Bases: BooleanFunction

Equivalence relation.

Equivalent(A, B) is True iff A and B are both True or both False

Returns True if all of the arguments are logically equivalent. Returns False otherwise.

Examples

>>> from .boolalg import Equivalent, And
>>> from ..abc import x, y
>>> Equivalent(False, False, False)
True
>>> Equivalent(True, False, False)
False
>>> Equivalent(x, And(x, True))
True

property args

Returns a tuple of arguments of ‘self’.

Examples

>>> from .. import cot
>>> from ..abc import x, y

>>> cot(x).args
(x,)

>>> cot(x).args[0]
x

>>> (x*y).args
(x, y)

>>> (x*y).args[1]
y

Notes

Never use self._args, always use self.args. Only use _args in __new__ when creating a new function. Don’t override .args() from Basic (so that it’s easy to change the interface in the future if needed).

default_assumptions = {}

to_nnf(simplify=True)

class modelparameters.sympy.logic.boolalg.ITE(*args)

Bases: BooleanFunction

If then else clause.

ITE(A, B, C) evaluates and returns the result of B if A is true else it returns the result of C

Examples

>>> from .boolalg import ITE, And, Xor, Or
>>> from ..abc import x, y, z
>>> ITE(True, False, True)
False
>>> ITE(Or(True, False), And(True, True), Xor(True, True))
True
>>> ITE(x, y, z)
ITE(x, y, z)
>>> ITE(True, x, y)
x
>>> ITE(False, x, y)
y
>>> ITE(x, y, y)
y

default_assumptions = {}

diff(*symbols, **assumptions)

classmethod eval(*args)

Returns a canonical form of cls applied to arguments args.

The eval() method is called when the class cls is about to be instantiated and it should return either some simplified instance (possible of some other class), or if the class cls should be unmodified, return None.

Examples of eval() for the function “sign”

@classmethod def eval(cls, arg):

if arg is S.NaN:

return S.NaN

if arg is S.Zero: return S.Zero if arg.is_positive: return S.One if arg.is_negative: return S.NegativeOne if isinstance(arg, Mul):

coeff, terms = arg.as_coeff_Mul(rational=True) if coeff is not S.One:

return cls(coeff) * cls(terms)

to_nnf(simplify=True)

class modelparameters.sympy.logic.boolalg.Implies(*args)

Bases: BooleanFunction

Logical implication.

A implies B is equivalent to !A v B

Accepts two Boolean arguments; A and B. Returns False if A is True and B is False Returns True otherwise.

Examples

>>> from .boolalg import Implies
>>> from .. import symbols
>>> x, y = symbols('x y')

>>> Implies(True, False)
False
>>> Implies(False, False)
True
>>> Implies(True, True)
True
>>> Implies(False, True)
True
>>> x >> y
Implies(x, y)
>>> y << x
Implies(x, y)

Notes

The >> and << operators are provided as a convenience, but note that their use here is different from their normal use in Python, which is bit shifts. Hence, Implies(a, b) and a >> b will return different things if a and b are integers. In particular, since Python considers True and False to be integers, True >> True will be the same as 1 >> 1, i.e., 0, which has a truth value of False. To avoid this issue, use the SymPy objects true and false.

>>> from .. import true, false
>>> True >> False
1
>>> true >> false
False

default_assumptions = {}

classmethod eval(*args)

Returns a canonical form of cls applied to arguments args.

The eval() method is called when the class cls is about to be instantiated and it should return either some simplified instance (possible of some other class), or if the class cls should be unmodified, return None.

Examples of eval() for the function “sign”

@classmethod def eval(cls, arg):

if arg is S.NaN:

return S.NaN

if arg is S.Zero: return S.Zero if arg.is_positive: return S.One if arg.is_negative: return S.NegativeOne if isinstance(arg, Mul):

coeff, terms = arg.as_coeff_Mul(rational=True) if coeff is not S.One:

return cls(coeff) * cls(terms)

to_nnf(simplify=True)

class modelparameters.sympy.logic.boolalg.Nand(*args)

Bases: BooleanFunction

Logical NAND function.

It evaluates its arguments in order, giving True immediately if any of them are False, and False if they are all True.

Returns True if any of the arguments are False Returns False if all arguments are True

Examples

>>> from .boolalg import Nand
>>> from .. import symbols
>>> x, y = symbols('x y')
>>> Nand(False, True)
True
>>> Nand(True, True)
False
>>> Nand(x, y)
~(x & y)

default_assumptions = {}

classmethod eval(*args)

Returns a canonical form of cls applied to arguments args.

The eval() method is called when the class cls is about to be instantiated and it should return either some simplified instance (possible of some other class), or if the class cls should be unmodified, return None.

Examples of eval() for the function “sign”

@classmethod def eval(cls, arg):

if arg is S.NaN:

return S.NaN

if arg is S.Zero: return S.Zero if arg.is_positive: return S.One if arg.is_negative: return S.NegativeOne if isinstance(arg, Mul):

coeff, terms = arg.as_coeff_Mul(rational=True) if coeff is not S.One:

return cls(coeff) * cls(terms)

class modelparameters.sympy.logic.boolalg.Nor(*args)

Bases: BooleanFunction

Logical NOR function.

It evaluates its arguments in order, giving False immediately if any of them are True, and True if they are all False.

Returns False if any argument is True Returns True if all arguments are False

Examples

>>> from .boolalg import Nor
>>> from .. import symbols
>>> x, y = symbols('x y')

>>> Nor(True, False)
False
>>> Nor(True, True)
False
>>> Nor(False, True)
False
>>> Nor(False, False)
True
>>> Nor(x, y)
~(x | y)

default_assumptions = {}

classmethod eval(*args)

Returns a canonical form of cls applied to arguments args.

The eval() method is called when the class cls is about to be instantiated and it should return either some simplified instance (possible of some other class), or if the class cls should be unmodified, return None.

Examples of eval() for the function “sign”

@classmethod def eval(cls, arg):

if arg is S.NaN:

return S.NaN

if arg is S.Zero: return S.Zero if arg.is_positive: return S.One if arg.is_negative: return S.NegativeOne if isinstance(arg, Mul):

coeff, terms = arg.as_coeff_Mul(rational=True) if coeff is not S.One:

return cls(coeff) * cls(terms)

class modelparameters.sympy.logic.boolalg.Not(arg)

Bases: BooleanFunction

Logical Not function (negation)

Returns True if the statement is False Returns False if the statement is True

Examples

>>> from .boolalg import Not, And, Or
>>> from ..abc import x, A, B
>>> Not(True)
False
>>> Not(False)
True
>>> Not(And(True, False))
True
>>> Not(Or(True, False))
False
>>> Not(And(And(True, x), Or(x, False)))
~x
>>> ~x
~x
>>> Not(And(Or(A, B), Or(~A, ~B)))
~((A | B) & (~A | ~B))

Notes

• The ~ operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise not. In particular, ~a and Not(a) will be different if a is an integer. Furthermore, since bools in Python subclass from int, ~True is the same as ~1 which is -2, which has a boolean value of True. To avoid this issue, use the SymPy boolean types true and false.

>>> from .. import true
>>> ~True
-2
>>> ~true
False

as_set()

Rewrite logic operators and relationals in terms of real sets.

Examples

>>> from .. import Not, Symbol
>>> x = Symbol('x', real=True)
>>> Not(x>0).as_set()
Interval(-oo, 0)

default_assumptions = {}

classmethod eval(arg)

Returns a canonical form of cls applied to arguments args.

The eval() method is called when the class cls is about to be instantiated and it should return either some simplified instance (possible of some other class), or if the class cls should be unmodified, return None.

Examples of eval() for the function “sign”

@classmethod def eval(cls, arg):

if arg is S.NaN:

return S.NaN

if arg is S.Zero: return S.Zero if arg.is_positive: return S.One if arg.is_negative: return S.NegativeOne if isinstance(arg, Mul):

coeff, terms = arg.as_coeff_Mul(rational=True) if coeff is not S.One:

return cls(coeff) * cls(terms)

is_Not = True

to_nnf(simplify=True)

class modelparameters.sympy.logic.boolalg.Or(*args)

Bases: LatticeOp, BooleanFunction

Logical OR function

It evaluates its arguments in order, giving True immediately if any of them are True, and False if they are all False.

Examples

>>> from ..core import symbols
>>> from ..abc import x, y
>>> from .boolalg import Or
>>> x | y
x | y

Notes

The | operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise or. Hence, Or(a, b) and a | b will return different things if a and b are integers.

>>> Or(x, y).subs(x, 0)
y

as_set()

Rewrite logic operators and relationals in terms of real sets.

Examples

>>> from .. import Or, Symbol
>>> x = Symbol('x', real=True)
>>> Or(x>2, x<-2).as_set()
Union(Interval.open(-oo, -2), Interval.open(2, oo))

default_assumptions = {'commutative': True}

identity = False

is_commutative

zero = True

modelparameters.sympy.logic.boolalg.POSform(variables, minterms, dontcares=None)

The POSform function uses simplified_pairs and a redundant-group eliminating algorithm to convert the list of all input combinations that generate ‘1’ (the minterms) into the smallest Product of Sums form.

The variables must be given as the first argument.

Return a logical And function (i.e., the “product of sums” or “POS” form) that gives the desired outcome. If there are inputs that can be ignored, pass them as a list, too.

The result will be one of the (perhaps many) functions that satisfy the conditions.

Examples

>>> from ..logic import POSform
>>> from .. import symbols
>>> w, x, y, z = symbols('w x y z')
>>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1], [0, 1, 1, 1],
...             [1, 0, 1, 1], [1, 1, 1, 1]]
>>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]
>>> POSform([w, x, y, z], minterms, dontcares)
z & (y | ~w)

References

[1]

en.wikipedia.org/wiki/Quine-McCluskey_algorithm

modelparameters.sympy.logic.boolalg.SOPform(variables, minterms, dontcares=None)

The SOPform function uses simplified_pairs and a redundant group- eliminating algorithm to convert the list of all input combos that generate ‘1’ (the minterms) into the smallest Sum of Products form.

The variables must be given as the first argument.

Return a logical Or function (i.e., the “sum of products” or “SOP” form) that gives the desired outcome. If there are inputs that can be ignored, pass them as a list, too.

The result will be one of the (perhaps many) functions that satisfy the conditions.

Examples

>>> from ..logic import SOPform
>>> from .. import symbols
>>> w, x, y, z = symbols('w x y z')
>>> minterms = [[0, 0, 0, 1], [0, 0, 1, 1],
...             [0, 1, 1, 1], [1, 0, 1, 1], [1, 1, 1, 1]]
>>> dontcares = [[0, 0, 0, 0], [0, 0, 1, 0], [0, 1, 0, 1]]
>>> SOPform([w, x, y, z], minterms, dontcares)
(y & z) | (z & ~w)

References

[1]

en.wikipedia.org/wiki/Quine-McCluskey_algorithm

class modelparameters.sympy.logic.boolalg.Xnor(*args)

Bases: BooleanFunction

Logical XNOR function.

Returns False if an odd number of the arguments are True and the rest are False.

Returns True if an even number of the arguments are True and the rest are False.

Examples

>>> from .boolalg import Xnor
>>> from .. import symbols
>>> x, y = symbols('x y')
>>> Xnor(True, False)
False
>>> Xnor(True, True)
True
>>> Xnor(True, False, True, True, False)
False
>>> Xnor(True, False, True, False)
True

default_assumptions = {}

classmethod eval(*args)

Returns a canonical form of cls applied to arguments args.

The eval() method is called when the class cls is about to be instantiated and it should return either some simplified instance (possible of some other class), or if the class cls should be unmodified, return None.

Examples of eval() for the function “sign”

@classmethod def eval(cls, arg):

if arg is S.NaN:

return S.NaN

if arg is S.Zero: return S.Zero if arg.is_positive: return S.One if arg.is_negative: return S.NegativeOne if isinstance(arg, Mul):

coeff, terms = arg.as_coeff_Mul(rational=True) if coeff is not S.One:

return cls(coeff) * cls(terms)

class modelparameters.sympy.logic.boolalg.Xor(*args)

Bases: BooleanFunction

Logical XOR (exclusive OR) function.

Returns True if an odd number of the arguments are True and the rest are False.

Returns False if an even number of the arguments are True and the rest are False.

Examples

>>> from .boolalg import Xor
>>> from .. import symbols
>>> x, y = symbols('x y')
>>> Xor(True, False)
True
>>> Xor(True, True)
False
>>> Xor(True, False, True, True, False)
True
>>> Xor(True, False, True, False)
False
>>> x ^ y
Xor(x, y)

Notes

The ^ operator is provided as a convenience, but note that its use here is different from its normal use in Python, which is bitwise xor. In particular, a ^ b and Xor(a, b) will be different if a and b are integers.

>>> Xor(x, y).subs(y, 0)
x

property args

Returns a tuple of arguments of ‘self’.

Examples

>>> from .. import cot
>>> from ..abc import x, y

>>> cot(x).args
(x,)

>>> cot(x).args[0]
x

>>> (x*y).args
(x, y)

>>> (x*y).args[1]
y

Notes

Never use self._args, always use self.args. Only use _args in __new__ when creating a new function. Don’t override .args() from Basic (so that it’s easy to change the interface in the future if needed).

default_assumptions = {}

to_nnf(simplify=True)

modelparameters.sympy.logic.boolalg.bool_map(bool1, bool2)

Return the simplified version of bool1, and the mapping of variables that makes the two expressions bool1 and bool2 represent the same logical behaviour for some correspondence between the variables of each. If more than one mappings of this sort exist, one of them is returned. For example, And(x, y) is logically equivalent to And(a, b) for the mapping {x: a, y:b} or {x: b, y:a}. If no such mapping exists, return False.

Examples

>>> from .. import SOPform, bool_map, Or, And, Not, Xor
>>> from ..abc import w, x, y, z, a, b, c, d
>>> function1 = SOPform([x, z, y],[[1, 0, 1], [0, 0, 1]])
>>> function2 = SOPform([a, b, c],[[1, 0, 1], [1, 0, 0]])
>>> bool_map(function1, function2)
(y & ~z, {y: a, z: b})

The results are not necessarily unique, but they are canonical. Here, (w, z) could be (a, d) or (d, a):

>>> eq =  Or(And(Not(y), w), And(Not(y), z), And(x, y))
>>> eq2 = Or(And(Not(c), a), And(Not(c), d), And(b, c))
>>> bool_map(eq, eq2)
((x & y) | (w & ~y) | (z & ~y), {w: a, x: b, y: c, z: d})
>>> eq = And(Xor(a, b), c, And(c,d))
>>> bool_map(eq, eq.subs(c, x))
(c & d & (a | b) & (~a | ~b), {a: a, b: b, c: d, d: x})

modelparameters.sympy.logic.boolalg.conjuncts(expr)

Return a list of the conjuncts in the expr s.

Examples

>>> from .boolalg import conjuncts
>>> from ..abc import A, B
>>> conjuncts(A & B)
frozenset({A, B})
>>> conjuncts(A | B)
frozenset({A | B})

modelparameters.sympy.logic.boolalg.disjuncts(expr)

Return a list of the disjuncts in the sentence s.

Examples

>>> from .boolalg import disjuncts
>>> from ..abc import A, B
>>> disjuncts(A | B)
frozenset({A, B})
>>> disjuncts(A & B)
frozenset({A & B})

modelparameters.sympy.logic.boolalg.distribute_and_over_or(expr)

Given a sentence s consisting of conjunctions and disjunctions of literals, return an equivalent sentence in CNF.

Examples

>>> from .boolalg import distribute_and_over_or, And, Or, Not
>>> from ..abc import A, B, C
>>> distribute_and_over_or(Or(A, And(Not(B), Not(C))))
(A | ~B) & (A | ~C)

modelparameters.sympy.logic.boolalg.distribute_or_over_and(expr)

Given a sentence s consisting of conjunctions and disjunctions of literals, return an equivalent sentence in DNF.

Note that the output is NOT simplified.

Examples

>>> from .boolalg import distribute_or_over_and, And, Or, Not
>>> from ..abc import A, B, C
>>> distribute_or_over_and(And(Or(Not(A), B), C))
(B & C) | (C & ~A)

modelparameters.sympy.logic.boolalg.eliminate_implications(expr)

Change >>, <<, and Equivalent into &, |, and ~. That is, return an expression that is equivalent to s, but has only &, |, and ~ as logical operators.

Examples

>>> from .boolalg import Implies, Equivalent,          eliminate_implications
>>> from ..abc import A, B, C
>>> eliminate_implications(Implies(A, B))
B | ~A
>>> eliminate_implications(Equivalent(A, B))
(A | ~B) & (B | ~A)
>>> eliminate_implications(Equivalent(A, B, C))
(A | ~C) & (B | ~A) & (C | ~B)

modelparameters.sympy.logic.boolalg.integer_to_term(k, n_bits=None)

Return a list of the base-2 digits in the integer, k.

Parameters:

• k (int) –

• n_bits (int) – If n_bits is given and the number of digits in the binary representation of k is smaller than n_bits then left-pad the list with 0s.

Examples

>>> from .boolalg import integer_to_term
>>> integer_to_term(4)
[1, 0, 0]
>>> integer_to_term(4, 6)
[0, 0, 0, 1, 0, 0]

modelparameters.sympy.logic.boolalg.is_cnf(expr)

Test whether or not an expression is in conjunctive normal form.

Examples

>>> from .boolalg import is_cnf
>>> from ..abc import A, B, C
>>> is_cnf(A | B | C)
True
>>> is_cnf(A & B & C)
True
>>> is_cnf((A & B) | C)
False

modelparameters.sympy.logic.boolalg.is_dnf(expr)

Test whether or not an expression is in disjunctive normal form.

Examples

>>> from .boolalg import is_dnf
>>> from ..abc import A, B, C
>>> is_dnf(A | B | C)
True
>>> is_dnf(A & B & C)
True
>>> is_dnf((A & B) | C)
True
>>> is_dnf(A & (B | C))
False

modelparameters.sympy.logic.boolalg.is_literal(expr)

Returns True if expr is a literal, else False.

Examples

>>> from .. import Or, Q
>>> from ..abc import A, B
>>> from .boolalg import is_literal
>>> is_literal(A)
True
>>> is_literal(~A)
True
>>> is_literal(Q.zero(A))
True
>>> is_literal(A + B)
True
>>> is_literal(Or(A, B))
False

modelparameters.sympy.logic.boolalg.is_nnf(expr, simplified=True)

Checks if expr is in Negation Normal Form. A logical expression is in Negation Normal Form (NNF) if it contains only And, Or and Not, and Not is applied only to literals. If simpified is True, checks if result contains no redundant clauses.

Examples

>>> from ..abc import A, B, C
>>> from .boolalg import Not, is_nnf
>>> is_nnf(A & B | ~C)
True
>>> is_nnf((A | ~A) & (B | C))
False
>>> is_nnf((A | ~A) & (B | C), False)
True
>>> is_nnf(Not(A & B) | C)
False
>>> is_nnf((A >> B) & (B >> A))
False

modelparameters.sympy.logic.boolalg.simplify_logic(expr, form=None, deep=True)

This function simplifies a boolean function to its simplified version in SOP or POS form. The return type is an Or or And object in SymPy.

Parameters:

• expr (string or boolean expression) –

• form (string ('cnf' or 'dnf') or None (default).) – If ‘cnf’ or ‘dnf’, the simplest expression in the corresponding normal form is returned; if None, the answer is returned according to the form with fewest args (in CNF by default).

• deep (boolean (default True)) – indicates whether to recursively simplify any non-boolean functions contained within the input.

Examples

>>> from ..logic import simplify_logic
>>> from ..abc import x, y, z
>>> from .. import S
>>> b = (~x & ~y & ~z) | ( ~x & ~y & z)
>>> simplify_logic(b)
~x & ~y

>>> S(b)
(z & ~x & ~y) | (~x & ~y & ~z)
>>> simplify_logic(_)
~x & ~y

modelparameters.sympy.logic.boolalg.term_to_integer(term)

Return an integer corresponding to the base-2 digits given by term.

Parameters:

term (a string or list of ones and zeros) –

Examples

>>> from .boolalg import term_to_integer
>>> term_to_integer([1, 0, 0])
4
>>> term_to_integer('100')
4

modelparameters.sympy.logic.boolalg.to_cnf(expr, simplify=False)

Convert a propositional logical sentence s to conjunctive normal form. That is, of the form ((A | ~B | …) & (B | C | …) & …) If simplify is True, the expr is evaluated to its simplest CNF form.

Examples

>>> from .boolalg import to_cnf
>>> from ..abc import A, B, D
>>> to_cnf(~(A | B) | D)
(D | ~A) & (D | ~B)
>>> to_cnf((A | B) & (A | ~A), True)
A | B

modelparameters.sympy.logic.boolalg.to_dnf(expr, simplify=False)

Convert a propositional logical sentence s to disjunctive normal form. That is, of the form ((A & ~B & …) | (B & C & …) | …) If simplify is True, the expr is evaluated to its simplest DNF form.

Examples

>>> from .boolalg import to_dnf
>>> from ..abc import A, B, C
>>> to_dnf(B & (A | C))
(A & B) | (B & C)
>>> to_dnf((A & B) | (A & ~B) | (B & C) | (~B & C), True)
A | C

modelparameters.sympy.logic.boolalg.to_int_repr(clauses, symbols)

Takes clauses in CNF format and puts them into an integer representation.

Examples

>>> from .boolalg import to_int_repr
>>> from ..abc import x, y
>>> to_int_repr([x | y, y], [x, y]) == [{1, 2}, {2}]
True

modelparameters.sympy.logic.boolalg.to_nnf(expr, simplify=True)

Converts expr to Negation Normal Form. A logical expression is in Negation Normal Form (NNF) if it contains only And, Or and Not, and Not is applied only to literals. If simplify is True, the result contains no redundant clauses.

Examples

>>> from ..abc import A, B, C, D
>>> from .boolalg import Not, Equivalent, to_nnf
>>> to_nnf(Not((~A & ~B) | (C & D)))
(A | B) & (~C | ~D)
>>> to_nnf(Equivalent(A >> B, B >> A))
(A | ~B | (A & ~B)) & (B | ~A | (B & ~A))

modelparameters.sympy.logic.boolalg.truth_table(expr, variables, input=True)

Return a generator of all possible configurations of the input variables, and the result of the boolean expression for those values.

Parameters:

• expr (string or boolean expression) –

• variables (list of variables) –

• input (boolean (default True)) – indicates whether to return the input combinations.

Examples

>>> from .boolalg import truth_table
>>> from ..abc import x,y
>>> table = truth_table(x >> y, [x, y])
>>> for t in table:
...     print('{0} -> {1}'.format(*t))
[0, 0] -> True
[0, 1] -> True
[1, 0] -> False
[1, 1] -> True

>>> table = truth_table(x | y, [x, y])
>>> list(table)
[([0, 0], False), ([0, 1], True), ([1, 0], True), ([1, 1], True)]

If input is false, truth_table returns only a list of truth values. In this case, the corresponding input values of variables can be deduced from the index of a given output.

>>> from .boolalg import integer_to_term
>>> vars = [y, x]
>>> values = truth_table(x >> y, vars, input=False)
>>> values = list(values)
>>> values
[True, False, True, True]

>>> for i, value in enumerate(values):
...     print('{0} -> {1}'.format(list(zip(
...     vars, integer_to_term(i, len(vars)))), value))
[(y, 0), (x, 0)] -> True
[(y, 0), (x, 1)] -> False
[(y, 1), (x, 0)] -> True
[(y, 1), (x, 1)] -> True

modelparameters.sympy.logic.inference module

Inference in propositional logic

class modelparameters.sympy.logic.inference.KB(sentence=None)

Bases: object

Base class for all knowledge bases

ask(query)

property clauses

retract(sentence)

tell(sentence)

class modelparameters.sympy.logic.inference.PropKB(sentence=None)

Bases: KB

A KB for Propositional Logic. Inefficient, with no indexing.

ask(query)

Checks if the query is true given the set of clauses.

Examples

>>> from .inference import PropKB
>>> from ..abc import x, y
>>> l = PropKB()
>>> l.tell(x & ~y)
>>> l.ask(x)
True
>>> l.ask(y)
False

retract(sentence)

Remove the sentence’s clauses from the KB

Examples

>>> from .inference import PropKB
>>> from ..abc import x, y
>>> l = PropKB()
>>> l.clauses
[]

>>> l.tell(x | y)
>>> l.clauses
[x | y]

>>> l.retract(x | y)
>>> l.clauses
[]

tell(sentence)

Add the sentence’s clauses to the KB

Examples

>>> from .inference import PropKB
>>> from ..abc import x, y
>>> l = PropKB()
>>> l.clauses
[]

>>> l.tell(x | y)
>>> l.clauses
[x | y]

>>> l.tell(y)
>>> l.clauses
[y, x | y]

modelparameters.sympy.logic.inference.entails(expr, formula_set={})

Check whether the given expr_set entail an expr. If formula_set is empty then it returns the validity of expr.

Examples

>>> from ..abc import A, B, C
>>> from .inference import entails
>>> entails(A, [A >> B, B >> C])
False
>>> entails(C, [A >> B, B >> C, A])
True
>>> entails(A >> B)
False
>>> entails(A >> (B >> A))
True

References

[1]

http://en.wikipedia.org/wiki/Logical_consequence

modelparameters.sympy.logic.inference.literal_symbol(literal)

The symbol in this literal (without the negation).

Examples

>>> from ..abc import A
>>> from .inference import literal_symbol
>>> literal_symbol(A)
A
>>> literal_symbol(~A)
A

modelparameters.sympy.logic.inference.pl_true(expr, model={}, deep=False)

Returns whether the given assignment is a model or not.

If the assignment does not specify the value for every proposition, this may return None to indicate ‘not obvious’.

Parameters:

• model (dict, optional, default: {}) – Mapping of symbols to boolean values to indicate assignment.

• deep (boolean, optional, default: False) – Gives the value of the expression under partial assignments correctly. May still return None to indicate ‘not obvious’.

Examples

>>> from ..abc import A, B, C
>>> from .inference import pl_true
>>> pl_true( A & B, {A: True, B: True})
True
>>> pl_true(A & B, {A: False})
False
>>> pl_true(A & B, {A: True})
>>> pl_true(A & B, {A: True}, deep=True)
>>> pl_true(A >> (B >> A))
>>> pl_true(A >> (B >> A), deep=True)
True
>>> pl_true(A & ~A)
>>> pl_true(A & ~A, deep=True)
False
>>> pl_true(A & B & (~A | ~B), {A: True})
>>> pl_true(A & B & (~A | ~B), {A: True}, deep=True)
False

modelparameters.sympy.logic.inference.satisfiable(expr, algorithm='dpll2', all_models=False)

Check satisfiability of a propositional sentence. Returns a model when it succeeds. Returns {true: true} for trivially true expressions.

On setting all_models to True, if given expr is satisfiable then returns a generator of models. However, if expr is unsatisfiable then returns a generator containing the single element False.

Examples

>>> from ..abc import A, B
>>> from .inference import satisfiable
>>> satisfiable(A & ~B)
{A: True, B: False}
>>> satisfiable(A & ~A)
False
>>> satisfiable(True)
{True: True}
>>> next(satisfiable(A & ~A, all_models=True))
False
>>> models = satisfiable((A >> B) & B, all_models=True)
>>> next(models)
{A: False, B: True}
>>> next(models)
{A: True, B: True}
>>> def use_models(models):
...     for model in models:
...         if model:
...             # Do something with the model.
...             print(model)
...         else:
...             # Given expr is unsatisfiable.
...             print("UNSAT")
>>> use_models(satisfiable(A >> ~A, all_models=True))
{A: False}
>>> use_models(satisfiable(A ^ A, all_models=True))
UNSAT

modelparameters.sympy.logic.inference.valid(expr)

Check validity of a propositional sentence. A valid propositional sentence is True under every assignment.

Examples

>>> from ..abc import A, B
>>> from .inference import valid
>>> valid(A | ~A)
True
>>> valid(A | B)
False

References

[1]

http://en.wikipedia.org/wiki/Validity

Module contents