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)  (z & ~w)
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)  (z & ~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}] >>> 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)  (x & y & z)  (~w & ~y)
References

sympy.logic.boolalg.
POSform
(variables, minterms, dontcares=None)[source]¶ The POSform function uses simplified_pairs and a redundantgroup 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)
References
Boolean functions¶

class
sympy.logic.boolalg.
BooleanTrue
(*args, **kwargs)[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 whenS.true
should be used in various contexts throughout SymPy. An important thing to remember is thatsympify(True)
returnsS.true
. This means that for the most part, you can just useTrue
and it will automatically be converted toS.true
when necessary, similar to how you can generally use 1 instead ofS.One
.The rule of thumb is:
“If the boolean in question can be replaced by an arbitrary symbolic
Boolean
, likeOr(x, y)
orx > 1
, useS.true
. Otherwise, useTrue
”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 beS.true
instead ofTrue
, as elements of.args
must beBasic
. On the other hand,==
is not a symbolic operation in SymPy, since it always returnsTrue
orFalse
, and does so in terms of structural equality rather than mathematical, so it should returnTrue
. The assumptions system should useTrue
andFalse
. Aside from not satisfying the above rule of thumb, the assumptions system uses a threevalued logic (True
,False
,None
), whereasS.true
andS.false
represent a twovalued logic. When in doubt, useTrue
.“
S.true == True is True
.”While “
S.true is True
” isFalse
, “S.true == True
” isTrue
, so if there is any doubt over whether a function or expression will returnS.true
orTrue
, just use==
instead ofis
to do the comparison, and it will work in either case. Finally, for boolean flags, it’s better to just useif x
instead ofif x is True
. To quote PEP 8:Don’t compare boolean values to
True
orFalse
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)
Python operators give a boolean result for true but a bitwise result for True
>>> ~true, ~True (False, 2) >>> true >> true, True >> True (True, 0)
See also

class
sympy.logic.boolalg.
BooleanFalse
(*args, **kwargs)[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 note in :py:class`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)
See also

class
sympy.logic.boolalg.
And
(*args, **options)[source]¶ 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 sympy.abc import x, y >>> from sympy.logic.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)
anda & b
will return different things ifa
andb
are integers.>>> And(x, y).subs(x, 1) y

class
sympy.logic.boolalg.
Or
(*args, **options)[source]¶ 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 sympy.abc import x, y >>> from sympy.logic.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)
anda  b
will return different things ifa
andb
are integers.>>> Or(x, y).subs(x, 0) y

class
sympy.logic.boolalg.
Not
(**kwargs)[source]¶ Logical Not function (negation)
Returns True if the statement is False Returns False if the statement is True
Examples
>>> from sympy.logic.boolalg 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
andNot(a)
will be different ifa
is an integer. Furthermore, since bools in Python subclass fromint
,~True
is the same as~1
which is2
, which has a boolean value of True. To avoid this issue, use the SymPy boolean typestrue
andfalse
.
>>> from sympy import true >>> ~True 2 >>> ~true False

class
sympy.logic.boolalg.
Xor
(*args, remove_true=True, **kwargs)[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
andXor(a, b)
will be different ifa
andb
are integers.>>> Xor(x, y).subs(y, 0) x

class
sympy.logic.boolalg.
Nand
(**kwargs)[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
(**kwargs)[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.
Implies
(**kwargs)[source]¶ 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 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)
anda >> b
will return different things ifa
andb
are integers. In particular, since Python considersTrue
andFalse
to be integers,True >> True
will be the same as1 >> 1
, i.e., 0, which has a truth value of False. To avoid this issue, use the SymPy objectstrue
andfalse
.>>> from sympy import true, false >>> True >> False 1 >>> true >> false False

class
sympy.logic.boolalg.
Equivalent
(*args, **options)[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.
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, **kwargs)[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.
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 nonBoolean args will generate a TypeError:
>>> ITE(True, [], ()) Traceback (most recent call last): ... TypeError: expecting bool, Boolean or ITE, not `[]`
The following functions can be used to handle Conjunctive and Disjunctive Normal forms

sympy.logic.boolalg.
to_cnf
(expr, simplify=False, force=False)[source]¶ Convert a propositional logical sentence s to conjunctive normal form: ((A  ~B  …) & (B  C  …) & …). If simplify is True, the expr is evaluated to its simplest CNF form using the QuineMcCluskey algorithm; this may take a long time if there are more than 8 variables and requires that the
force
flag be set to True (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 s to disjunctive normal form: ((A & ~B & …)  (B & C & …)  …). If simplify is True, the expr is evaluated to its simplest DNF form using the QuineMcCluskey algorithm; this may take a long time if there are more than 8 variables and requires that the
force
flag be set to True (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.
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
Simplification and equivalencetesting¶

sympy.logic.boolalg.
simplify_logic
(expr, form=None, deep=True, force=False)[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 : 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 nonboolean functions contained within the input.
force : boolean (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 toTrue
, this limit is removed. Be aware that this can lead to very long simplification times.
Examples
>>> from sympy.logic import simplify_logic >>> from sympy.abc import x, y, z >>> from sympy 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
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})
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)[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