Logic

Introduction

The logic module for SymPy allows to form and manipulate logic expressions using symbolic and Boolean values.

Forming logical expressions

You can build Boolean expressions with the standard python operators & (And), | (Or), ~ (Not):

>>> from sympy import *
>>> x, y = symbols('x,y')
>>> y | (x & y)
y | (x & y)
>>> x | y
x | y
>>> ~x
~x

You can also form implications with >> and <<:

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

Like most types in SymPy, Boolean expressions inherit from Basic:

>>> (y & x).subs({x: True, y: True})
True
>>> (x | y).atoms()
{x, y}

The logic module also includes the following functions to derive boolean expressions from their truth tables:

sympy.logic.boolalg.SOPform(variables, minterms, dontcares=None)[source]

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 sympy.logic import SOPform
>>> from sympy 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) | (~w & ~x)

The terms can also be represented as integers:

>>> minterms = [1, 3, 7, 11, 15]
>>> dontcares = [0, 2, 5]
>>> SOPform([w, x, y, z], minterms, dontcares)
(y & z) | (~w & ~x)

They can also be specified using dicts, which does not have to be fully specified:

>>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}]
>>> SOPform([w, x, y, z], minterms)
(x & ~w) | (y & z & ~x)

Or a combination:

>>> minterms = [4, 7, 11, [1, 1, 1, 1]]
>>> dontcares = [{w : 0, x : 0, y: 0}, 5]
>>> SOPform([w, x, y, z], minterms, dontcares)
(w & y & z) | (~w & ~y) | (x & z & ~w)

See also

POSform

References

sympy.logic.boolalg.POSform(variables, minterms, dontcares=None)[source]

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 sympy.logic import POSform
>>> from sympy 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)

The terms can also be represented as integers:

>>> minterms = [1, 3, 7, 11, 15]
>>> dontcares = [0, 2, 5]
>>> POSform([w, x, y, z], minterms, dontcares)
z & (y | ~w)

They can also be specified using dicts, which does not have to be fully specified:

>>> minterms = [{w: 0, x: 1}, {y: 1, z: 1, x: 0}]
>>> POSform([w, x, y, z], minterms)
(x | y) & (x | z) & (~w | ~x)

Or a combination:

>>> minterms = [4, 7, 11, [1, 1, 1, 1]]
>>> dontcares = [{w : 0, x : 0, y: 0}, 5]
>>> POSform([w, x, y, z], minterms, dontcares)
(w | x) & (y | ~w) & (z | ~y)

See also

SOPform

References

sympy.logic.boolalg.ANFform(variables, truthvalues)[source]

The ANFform function converts the list of truth values to Algebraic Normal Form (ANF).

The variables must be given as the first argument.

Return True, False, logical And function (i.e., the “Zhegalkin monomial”) or logical Xor function (i.e., the “Zhegalkin polynomial”). When True and False are represented by 1 and 0, respectively, then And is multiplication and Xor is addition.

Formally a “Zhegalkin monomial” is the product (logical And) of a finite set of distinct variables, including the empty set whose product is denoted 1 (True). A “Zhegalkin polynomial” is the sum (logical Xor) of a set of Zhegalkin monomials, with the empty set denoted by 0 (False).

Parameters:

variables : list of variables

truthvalues : list of 1’s and 0’s (result column of truth table)

Examples

>>> from sympy.logic.boolalg import ANFform
>>> from sympy.abc import x, y
>>> ANFform([x], [1, 0])
x ^ True
>>> ANFform([x, y], [0, 1, 1, 1])
x ^ y ^ (x & y)

References

Boolean functions

class sympy.logic.boolalg.Boolean(*args)[source]

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

as_set()[source]

Rewrites Boolean expression in terms of real sets.

Examples

>>> from sympy import Symbol, Eq, Or, And
>>> x = Symbol('x', real=True)
>>> Eq(x, 0).as_set()
{0}
>>> (x > 0).as_set()
Interval.open(0, oo)
>>> And(-2 < x, x < 2).as_set()
Interval.open(-2, 2)
>>> Or(x < -2, 2 < x).as_set()
Union(Interval.open(-oo, -2), Interval.open(2, oo))
equals(other)[source]

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 sympy.abc import A, B, C
>>> from sympy 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 sympy.logic.boolalg.BooleanTrue[source]

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:

Do not compare boolean values to True or False using ==.

  • Yes: if greeting:

  • No: if greeting == True:

  • Worse: if greeting is True:

Examples

>>> from sympy import sympify, true, false, Or
>>> sympify(True)
True
>>> _ is True, _ is true
(False, True)
>>> Or(true, false)
True
>>> _ is true
True

Python operators give a boolean result for true but a bitwise result for True

>>> ~true, ~True  
(False, -2)
>>> true >> true, True >> True
(True, 0)
as_set()[source]

Rewrite logic operators and relationals in terms of real sets.

Examples

>>> from sympy import true
>>> true.as_set()
UniversalSet
class sympy.logic.boolalg.BooleanFalse[source]

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 the notes section in sympy.logic.boolalg.BooleanTrue

Examples

>>> from sympy import sympify, true, false, Or
>>> sympify(False)
False
>>> _ is False, _ is false
(False, True)
>>> Or(true, false)
True
>>> _ is true
True

Python operators give a boolean result for false but a bitwise result for False

>>> ~false, ~False  
(True, -1)
>>> false >> false, False >> False
(True, 0)
as_set()[source]

Rewrite logic operators and relationals in terms of real sets.

Examples

>>> from sympy import false
>>> false.as_set()
EmptySet
class sympy.logic.boolalg.And(*args)[source]

Logical AND function.

It evaluates its arguments in order, returning false immediately when an argument is false and true if they are all true.

Examples

>>> from sympy.abc import x, y
>>> from sympy 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 produce different results if a and b are integers.

>>> And(x, y).subs(x, 1)
y
class sympy.logic.boolalg.Or(*args)[source]

Logical OR function

It evaluates its arguments in order, returning true immediately when an argument is true, and false if they are all false.

Examples

>>> from sympy.abc import x, y
>>> from sympy 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
class sympy.logic.boolalg.Not(arg)[source]

Logical Not function (negation)

Returns true if the statement is false or False. Returns false if the statement is true or True.

Examples

>>> from sympy import Not, And, Or
>>> from sympy.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.

  • As of Python 3.12, the bitwise not operator ~ used on a Python bool is deprecated and will emit a warning.

>>> from sympy import true
>>> ~True  
-2
>>> ~true
False
class sympy.logic.boolalg.Xor(*args)[source]

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 sympy.logic.boolalg import Xor
>>> from sympy 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
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
class sympy.logic.boolalg.Nand(*args)[source]

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 sympy.logic.boolalg import Nand
>>> from sympy import symbols
>>> x, y = symbols('x y')
>>> Nand(False, True)
True
>>> Nand(True, True)
False
>>> Nand(x, y)
~(x & y)
class sympy.logic.boolalg.Nor(*args)[source]

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 sympy.logic.boolalg import Nor
>>> from sympy 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)
class sympy.logic.boolalg.Xnor(*args)[source]

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 sympy.logic.boolalg import Xnor
>>> from sympy 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
class sympy.logic.boolalg.Implies(*args)[source]

Logical implication.

A implies B is equivalent to if A then B. Mathematically, it is written as \(A \Rightarrow B\) and is equivalent to \(\neg A \vee B\) or ~A | B.

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

Examples

>>> from sympy.logic.boolalg import Implies
>>> from sympy 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 sympy import true, false
>>> True >> False
1
>>> true >> false
False
class sympy.logic.boolalg.Equivalent(*args)[source]

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.

For two arguments, this is equivalent to Xnor.

Examples

>>> from sympy.logic.boolalg import Equivalent, And
>>> from sympy.abc import x
>>> Equivalent(False, False, False)
True
>>> Equivalent(True, False, False)
False
>>> Equivalent(x, And(x, True))
True
class sympy.logic.boolalg.ITE(*args)[source]

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. All args must be Booleans.

From a logic gate perspective, ITE corresponds to a 2-to-1 multiplexer, where A is the select signal.

Examples

>>> from sympy.logic.boolalg import ITE, And, Xor, Or
>>> from sympy.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

Trying to use non-Boolean args will generate a TypeError:

>>> ITE(True, [], ())
Traceback (most recent call last):
...
TypeError: expecting bool, Boolean or ITE, not `[]`
class sympy.logic.boolalg.Exclusive(*args)[source]

True if only one or no argument is true.

Exclusive(A, B, C) is equivalent to ~(A & B) & ~(A & C) & ~(B & C).

For two arguments, this is equivalent to Xor.

Examples

>>> from sympy.logic.boolalg import Exclusive
>>> Exclusive(False, False, False)
True
>>> Exclusive(False, True, False)
True
>>> Exclusive(False, True, True)
False

The following functions can be used to handle Algebraic, Conjunctive, Disjunctive, and Negated Normal forms:

sympy.logic.boolalg.to_anf(expr, deep=True)[source]

Converts expr to Algebraic Normal Form (ANF).

ANF is a canonical normal form, which means that two equivalent formulas will convert to the same ANF.

A logical expression is in ANF if it has the form

\[1 \oplus a \oplus b \oplus ab \oplus abc\]
i.e. it can be:
  • purely true,

  • purely false,

  • conjunction of variables,

  • exclusive disjunction.

The exclusive disjunction can only contain true, variables or conjunction of variables. No negations are permitted.

If deep is False, arguments of the boolean expression are considered variables, i.e. only the top-level expression is converted to ANF.

Examples

>>> from sympy.logic.boolalg import And, Or, Not, Implies, Equivalent
>>> from sympy.logic.boolalg import to_anf
>>> from sympy.abc import A, B, C
>>> to_anf(Not(A))
A ^ True
>>> to_anf(And(Or(A, B), Not(C)))
A ^ B ^ (A & B) ^ (A & C) ^ (B & C) ^ (A & B & C)
>>> to_anf(Implies(Not(A), Equivalent(B, C)), deep=False)
True ^ ~A ^ (~A & (Equivalent(B, C)))
sympy.logic.boolalg.to_cnf(expr, simplify=False, force=False)[source]

Convert a propositional logical sentence expr to conjunctive normal form: ((A | ~B | ...) & (B | C | ...) & ...). If simplify is True, expr is evaluated to its simplest CNF form using the Quine-McCluskey algorithm; this may take a long time. If there are more than 8 variables the force flag must be set to True to simplify (default is False).

Examples

>>> from sympy.logic.boolalg import to_cnf
>>> from sympy.abc import A, B, D
>>> to_cnf(~(A | B) | D)
(D | ~A) & (D | ~B)
>>> to_cnf((A | B) & (A | ~A), True)
A | B
sympy.logic.boolalg.to_dnf(expr, simplify=False, force=False)[source]

Convert a propositional logical sentence expr to disjunctive normal form: ((A & ~B & ...) | (B & C & ...) | ...). If simplify is True, expr is evaluated to its simplest DNF form using the Quine-McCluskey algorithm; this may take a long time. If there are more than 8 variables, the force flag must be set to True to simplify (default is False).

Examples

>>> from sympy.logic.boolalg import to_dnf
>>> from sympy.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
sympy.logic.boolalg.to_nnf(expr, simplify=True)[source]

Converts expr to Negation Normal Form (NNF).

A logical expression is in 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 sympy.abc import A, B, C, D
>>> from sympy.logic.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))
sympy.logic.boolalg.is_anf(expr)[source]

Checks if expr is in Algebraic Normal Form (ANF).

A logical expression is in ANF if it has the form

\[1 \oplus a \oplus b \oplus ab \oplus abc\]

i.e. it is purely true, purely false, conjunction of variables or exclusive disjunction. The exclusive disjunction can only contain true, variables or conjunction of variables. No negations are permitted.

Examples

>>> from sympy.logic.boolalg import And, Not, Xor, true, is_anf
>>> from sympy.abc import A, B, C
>>> is_anf(true)
True
>>> is_anf(A)
True
>>> is_anf(And(A, B, C))
True
>>> is_anf(Xor(A, Not(B)))
False
sympy.logic.boolalg.is_cnf(expr)[source]

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

Examples

>>> from sympy.logic.boolalg import is_cnf
>>> from sympy.abc import A, B, C
>>> is_cnf(A | B | C)
True
>>> is_cnf(A & B & C)
True
>>> is_cnf((A & B) | C)
False
sympy.logic.boolalg.is_dnf(expr)[source]

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

Examples

>>> from sympy.logic.boolalg import is_dnf
>>> from sympy.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
sympy.logic.boolalg.is_nnf(expr, simplified=True)[source]

Checks if expr is in Negation Normal Form (NNF).

A logical expression is in NNF if it contains only And, Or and Not, and Not is applied only to literals. If simplified is True, checks if result contains no redundant clauses.

Examples

>>> from sympy.abc import A, B, C
>>> from sympy.logic.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
sympy.logic.boolalg.gateinputcount(expr)[source]

Return the total number of inputs for the logic gates realizing the Boolean expression.

Returns:

int

Number of gate inputs

Note

Not all Boolean functions count as gate here, only those that are considered to be standard gates. These are: And, Or, Xor, Not, and ITE (multiplexer). Nand, Nor, and Xnor will be evaluated to Not(And()) etc.

Examples

>>> from sympy.logic import And, Or, Nand, Not, gateinputcount
>>> from sympy.abc import x, y, z
>>> expr = And(x, y)
>>> gateinputcount(expr)
2
>>> gateinputcount(Or(expr, z))
4

Note that Nand is automatically evaluated to Not(And()) so

>>> gateinputcount(Nand(x, y, z))
4
>>> gateinputcount(Not(And(x, y, z)))
4

Although this can be avoided by using evaluate=False

>>> gateinputcount(Nand(x, y, z, evaluate=False))
3

Also note that a comparison will count as a Boolean variable:

>>> gateinputcount(And(x > z, y >= 2))
2

As will a symbol: >>> gateinputcount(x) 0

Simplification and equivalence-testing

sympy.logic.boolalg.simplify_logic(expr, form=None, deep=True, force=False, dontcare=None)[source]

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 : Boolean

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 : bool (default True)

Indicates whether to recursively simplify any non-boolean functions contained within the input.

force : bool (default False)

As the simplifications require exponential time in the number of variables, there is by default a limit on expressions with 8 variables. When the expression has more than 8 variables only symbolical simplification (controlled by deep) is made. By setting force to True, this limit is removed. Be aware that this can lead to very long simplification times.

dontcare : Boolean

Optimize expression under the assumption that inputs where this expression is true are don’t care. This is useful in e.g. Piecewise conditions, where later conditions do not need to consider inputs that are converted by previous conditions. For example, if a previous condition is And(A, B), the simplification of expr can be made with don’t cares for And(A, B).

Examples

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

References

SymPy’s simplify() function can also be used to simplify logic expressions to their simplest forms.

sympy.logic.boolalg.bool_map(bool1, bool2)[source]

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 sympy import SOPform, bool_map, Or, And, Not, Xor
>>> from sympy.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})

Manipulating expressions

The following functions can be used to manipulate Boolean expressions:

sympy.logic.boolalg.distribute_and_over_or(expr)[source]

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

Examples

>>> from sympy.logic.boolalg import distribute_and_over_or, And, Or, Not
>>> from sympy.abc import A, B, C
>>> distribute_and_over_or(Or(A, And(Not(B), Not(C))))
(A | ~B) & (A | ~C)
sympy.logic.boolalg.distribute_or_over_and(expr)[source]

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

Note that the output is NOT simplified.

Examples

>>> from sympy.logic.boolalg import distribute_or_over_and, And, Or, Not
>>> from sympy.abc import A, B, C
>>> distribute_or_over_and(And(Or(Not(A), B), C))
(B & C) | (C & ~A)
sympy.logic.boolalg.distribute_xor_over_and(expr)[source]

Given a sentence expr consisting of conjunction and exclusive disjunctions of literals, return an equivalent exclusive disjunction.

Note that the output is NOT simplified.

Examples

>>> from sympy.logic.boolalg import distribute_xor_over_and, And, Xor, Not
>>> from sympy.abc import A, B, C
>>> distribute_xor_over_and(And(Xor(Not(A), B), C))
(B & C) ^ (C & ~A)
sympy.logic.boolalg.eliminate_implications(expr)[source]

Change Implies and Equivalent into And, Or, and Not. That is, return an expression that is equivalent to expr, but has only &, |, and ~ as logical operators.

Examples

>>> from sympy.logic.boolalg import Implies, Equivalent,          eliminate_implications
>>> from sympy.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)

Inference

This module implements some inference routines in propositional logic.

The function satisfiable will test that a given Boolean expression is satisfiable, that is, you can assign values to the variables to make the sentence True.

For example, the expression x & ~x is not satisfiable, since there are no values for x that make this sentence True. On the other hand, (x | y) & (x | ~y) & (~x | y) is satisfiable with both x and y being True.

>>> from sympy.logic.inference import satisfiable
>>> from sympy import Symbol
>>> x = Symbol('x')
>>> y = Symbol('y')
>>> satisfiable(x & ~x)
False
>>> satisfiable((x | y) & (x | ~y) & (~x | y))
{x: True, y: True}

As you see, when a sentence is satisfiable, it returns a model that makes that sentence True. If it is not satisfiable it will return False.

sympy.logic.inference.satisfiable(expr, algorithm=None, all_models=False, minimal=False, use_lra_theory=False)[source]

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 sympy.abc import A, B
>>> from sympy.logic.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