逻辑

介绍

sypy的逻辑模块允许使用符号和布尔值来形成和操作逻辑表达式。

形成逻辑表达式

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

你也可以用 >> 和 << ：：

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

与SymPy中的大多数类型一样，布尔表达式继承自 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)

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.

变量必须作为第一个参数给定。

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.

结果将是满足条件的函数之一（可能是许多函数）。

实例

>>> 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)

这些术语也可以用整数表示：

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

也可以使用dicts指定它们，而不必完全指定：

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

或组合：

>>> 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)

参见

POSform

工具书类

[R600]

https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm

[R601]

https://en.wikipedia.org/wiki/Don%27t-care_term

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.

变量必须作为第一个参数给定。

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.

结果将是满足条件的函数之一（可能是许多函数）。

实例

>>> 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)

这些术语也可以用整数表示：

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

也可以使用dicts指定它们，而不必完全指定：

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

或组合：

>>> 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)

参见

SOPform

工具书类

[R602]

https://en.wikipedia.org/wiki/Quine-McCluskey_algorithm

[R603]

https://en.wikipedia.org/wiki/Don%27t-care_term

sympy.logic.boolalg.ANFform(variables, truthvalues)

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

变量必须作为第一个参数给定。

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).

参数:

variables : list of variables

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

实例

>>> 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)

工具书类

[R604]

https://en.wikipedia.org/wiki/Zhegalkin_polynomial

布尔函数

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

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

as_set()

Rewrites Boolean expression in terms of real sets.

实例

>>> 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)

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

实例

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

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.

笔记

至于什么时候可能会有些混乱 True 应该在什么时候使用 S.true 应该在不同的上下文中使用。重要的是要记住 sympify(True) 收益率 S.true . 这意味着在大多数情况下，您可以使用 True 将自动转换为 S.true 必要时，类似于通常使用1代替 S.One .

经验法则是：

“如果可以用任意符号替换所涉布尔值 Boolean ，像 Or(x, y) 或 x > 1 使用 S.true . 否则，使用 True “

换句话说，使用 S.true 只有在布尔值被用作真理的符号表示的情况下。例如，如果对象在 .args 那么它必然是 S.true 而不是 True ，作为元素 .args 必须是 Basic . 另一方面， == 不是SymPy中的符号操作，因为它总是返回 True 或 False ，并且是从结构平等的角度而不是数学的角度来做的，所以它应该返回 True . 假设系统应该使用 True 和 False . 除了不满足上述经验法则外，假设系统使用三值逻辑 (True ， False ， None )，鉴于 S.true 和 S.false 表示二值逻辑。如有疑问，请使用 True .

“\(S.true==true为true\)。”

而“\(S.true is true\)”则是 False ，“\(S.true==true`\)”是 True ，所以如果对函数或表达式是否返回有任何疑问 S.true 或 True 只是使用 == 而不是 is 做比较，在任何一种情况下都是有效的。最后，对于布尔标志，最好使用 if x 而不是 if x is True . 引用政治公众人物8：

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

• 对： if greeting:

• 不： if greeting == True:

• 更糟的是： if greeting is True:

实例

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

>>> Or(true, false)
True
>>> _ is true
True

Python运算符为true提供布尔结果，而为true提供按位结果

>>> ~true, ~True
(False, -2)
>>> true >> true, True >> True
(True, 0)

Python运算符为true提供布尔结果，而为true提供按位结果

>>> ~true, ~True
(False, -2)
>>> true >> true, True >> True
(True, 0)

参见

sympy.logic.boolalg.BooleanFalse

as_set()

Rewrite logic operators and relationals in terms of real sets.

实例

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

class sympy.logic.boolalg.BooleanFalse

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.

笔记

See the notes section in sympy.logic.boolalg.BooleanTrue

实例

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

>>> Or(true, false)
True
>>> _ is true
True

Python运算符为false提供布尔结果，而为false提供按位结果

>>> ~false, ~False
(True, -1)
>>> false >> false, False >> False
(True, 0)

参见

sympy.logic.boolalg.BooleanTrue

as_set()

Rewrite logic operators and relationals in terms of real sets.

实例

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

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

逻辑与功能。

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

实例

>>> from sympy.abc import x, y
>>> from sympy import And
>>> x & y
x & y

笔记

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)

逻辑或函数

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

实例

>>> from sympy.abc import x, y
>>> from sympy import Or
>>> x | y
x | y

笔记

这个 | 操作符是为了方便起见而提供的，但请注意，它在这里的用法不同于它在Python中的正常用法，即按位或。因此， Or(a, b) 和 a | b 会返回不同的东西如果 a 和 b 是整数。

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

class sympy.logic.boolalg.Not(arg)

逻辑非函数（否定）

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

实例

>>> 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))

笔记

• 这个 ~ 操作符是为了方便起见而提供的，但请注意，它在这里的用法不同于它在Python中的正常用法，而Python则不是按位的。特别地， ~a 和 Not(a) 如果 a 是一个整数。而且，因为 int ， ~True 是一样的 ~1 哪个是 -2 ，其布尔值为True。若要避免此问题，请使用SymPy布尔类型 true 和 false .

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

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

逻辑异或（异或）函数。

如果奇数个参数为True，其余参数为False，则返回True。

如果偶数个参数为True，其余参数为False，则返回False。

实例

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

笔记

这个 ^ 操作符是为了方便起见而提供的，但请注意，它在这里的用法不同于它在Python中的正常用法，即按位异或。特别地， a ^ b 和 Xor(a, b) 如果 a 和 b 是整数。

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

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

逻辑NAND函数。

它按顺序计算其参数，如果其中任何一个参数为False，则立即给出True；如果所有参数都为True，则返回False。

如果任何参数为False，则返回True；如果所有参数均为True，则返回False

实例

>>> 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)

逻辑或函数。

它按顺序计算其参数，如果其中任何一个为真，则立即给出False；如果所有参数都为False，则返回True。

如果任何参数为True，则返回False，如果所有参数都为False，则返回True

实例

>>> 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)

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.

实例

>>> 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)

逻辑含义。

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.

接受两个布尔参数；A和B。如果A为True，则返回False；B为False，否则返回True。

实例

>>> 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)

笔记

这个 >> 和 << 提供运算符是为了方便起见，但请注意，它们在这里的用法与Python中的正常用法不同，后者是位移位。因此， Implies(a, b) 和 a >> b 会返回不同的东西如果 a 和 b 是整数。特别是，由于Python考虑 True 和 False 作为整数， True >> True 将与 1 >> 1 ，即0，其真值为False。若要避免此问题，请使用SymPy对象 true 和 false .

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

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

等价关系。

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

如果所有参数在逻辑上等价，则返回True。否则返回False。

For two arguments, this is equivalent to Xnor.

实例

>>> 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)

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.

实例

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

尝试使用非布尔参数将生成类型错误：

>>> ITE(True, [], ())
Traceback (most recent call last):
...
TypeError: expecting bool, Boolean or ITE, not `[]`

class sympy.logic.boolalg.Exclusive(*args)

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.

实例

>>> 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)

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.

实例

>>> 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)

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).

实例

>>> 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)

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).

实例

>>> 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)

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.

实例

>>> 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)

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.

实例

>>> 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)

测试一个表达式是否为连接正常形式。

实例

>>> 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)

测试表达式是否为析取范式。

实例

>>> 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)

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.

实例

>>> 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)

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

返回:

利息

Number of gate inputs

注意

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.

实例

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

简化与等价性检验

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

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.

参数:

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)

指示是否要以非递归方式简化包含在任何布尔函数中的输入。

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).

实例

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

工具书类

[R605]

https://en.wikipedia.org/wiki/Don%27t-care_term

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

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.

实例

>>> 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})

它们不一定是唯一的，但不一定是唯一的。在这里， (w, z) 可以是 (a, d) 或 (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)

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

实例

>>> 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)

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

Note that the output is NOT simplified.

实例

>>> 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)

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

Note that the output is NOT simplified.

实例

>>> 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)

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.

实例

>>> 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)

Truth tables and related functions

It is possible to create a truth table for a Boolean function with

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.

参数:

expr : Boolean expression

variables : list of variables

input : bool (default True)

Indicates whether to return the input combinations.

实例

>>> from sympy.logic.boolalg import truth_table
>>> from sympy.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 sympy.utilities.iterables import ibin
>>> 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, ibin(i, len(vars)))), value))
[(y, 0), (x, 0)] -> True
[(y, 0), (x, 1)] -> False
[(y, 1), (x, 0)] -> True
[(y, 1), (x, 1)] -> True

For mapping between integer representations of truth table positions, lists of zeros and ones and symbols, the following functions can be used:

sympy.logic.boolalg.integer_to_term(n, bits=None, str=False)

返回长度列表 bits 对应于 n 在右边有一小段（最后）。如果省略位，则长度将是表示所需的数字 n . 如果所需位的顺序相反，则使用 [::-1] 返回列表的切片。

如果所有位长度列表的序列从 [0, 0,..., 0] 通过 [1, 1, ..., 1] 如果需要，则为位传递一个非整数，例如。 'all' .

如果钻头 一串 是期望通过 str=True .

实例

>>> from sympy.utilities.iterables import ibin
>>> ibin(2)
[1, 0]
>>> ibin(2, 4)
[0, 0, 1, 0]

如果所有列表对应0到2**n-1，则为位传递一个非整数：

>>> bits = 2
>>> for i in ibin(2, 'all'):
...     print(i)
(0, 0)
(0, 1)
(1, 0)
(1, 1)

如果需要给定长度的位字符串，请使用str=True：

>>> n = 123
>>> bits = 10
>>> ibin(n, bits, str=True)
'0001111011'
>>> ibin(n, bits, str=True)[::-1]  # small bits left
'1101111000'
>>> list(ibin(3, 'all', str=True))
['000', '001', '010', '011', '100', '101', '110', '111']

sympy.logic.boolalg.term_to_integer(term)

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

参数:

term : a string or list of ones and zeros

实例

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

sympy.logic.boolalg.bool_maxterm(k, variables)

Return the k-th maxterm.

Each maxterm is assigned an index based on the opposite conventional binary encoding used for minterms. The maxterm convention assigns the value 0 to the direct form and 1 to the complemented form.

参数:

k : int or list of 1's and 0's (complementation pattern)

variables : list of variables

实例

>>> from sympy.logic.boolalg import bool_maxterm
>>> from sympy.abc import x, y, z
>>> bool_maxterm([1, 0, 1], [x, y, z])
y | ~x | ~z
>>> bool_maxterm(6, [x, y, z])
z | ~x | ~y

工具书类

[R606]

https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_maxterms

sympy.logic.boolalg.bool_minterm(k, variables)

Return the k-th minterm.

Minterms are numbered by a binary encoding of the complementation pattern of the variables. This convention assigns the value 1 to the direct form and 0 to the complemented form.

参数:

k : int or list of 1's and 0's (complementation pattern)

variables : list of variables

实例

>>> from sympy.logic.boolalg import bool_minterm
>>> from sympy.abc import x, y, z
>>> bool_minterm([1, 0, 1], [x, y, z])
x & z & ~y
>>> bool_minterm(6, [x, y, z])
x & y & ~z

工具书类

[R607]

https://en.wikipedia.org/wiki/Canonical_normal_form#Indexing_minterms

sympy.logic.boolalg.bool_monomial(k, variables)

Return the k-th monomial.

Monomials are numbered by a binary encoding of the presence and absences of the variables. This convention assigns the value 1 to the presence of variable and 0 to the absence of variable.

Each boolean function can be uniquely represented by a Zhegalkin Polynomial (Algebraic Normal Form). The Zhegalkin Polynomial of the boolean function with \(n\) variables can contain up to \(2^n\) monomials. We can enumerate all the monomials. Each monomial is fully specified by the presence or absence of each variable.

For example, boolean function with four variables (a, b, c, d) can contain up to \(2^4 = 16\) monomials. The 13-th monomial is the product a & b & d, because 13 in binary is 1, 1, 0, 1.

参数:

k : int or list of 1's and 0's

variables : list of variables

实例

>>> from sympy.logic.boolalg import bool_monomial
>>> from sympy.abc import x, y, z
>>> bool_monomial([1, 0, 1], [x, y, z])
x & z
>>> bool_monomial(6, [x, y, z])
x & y

sympy.logic.boolalg.anf_coeffs(truthvalues)

Convert a list of truth values of some boolean expression to the list of coefficients of the polynomial mod 2 (exclusive disjunction) representing the boolean expression in ANF (i.e., the "Zhegalkin polynomial").

There are \(2^n\) possible Zhegalkin monomials in \(n\) variables, since each monomial is fully specified by the presence or absence of each variable.

We can enumerate all the monomials. For example, boolean function with four variables (a, b, c, d) can contain up to \(2^4 = 16\) monomials. The 13-th monomial is the product a & b & d, because 13 in binary is 1, 1, 0, 1.

A given monomial's presence or absence in a polynomial corresponds to that monomial's coefficient being 1 or 0 respectively.

实例

>>> from sympy.logic.boolalg import anf_coeffs, bool_monomial, Xor
>>> from sympy.abc import a, b, c
>>> truthvalues = [0, 1, 1, 0, 0, 1, 0, 1]
>>> coeffs = anf_coeffs(truthvalues)
>>> coeffs
[0, 1, 1, 0, 0, 0, 1, 0]
>>> polynomial = Xor(*[
...     bool_monomial(k, [a, b, c])
...     for k, coeff in enumerate(coeffs) if coeff == 1
... ])
>>> polynomial
b ^ c ^ (a & b)

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

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

实例

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

推论

该模块实现了命题逻辑中的一些推理程序。

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.

例如，表达式 x & ~x 不可满足，因为没有 x 这就是这个句子 True . 另一方面， (x | y) & (x | ~y) & (~x | y) 两者都能满足 x 和 y 存在 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}

如您所见，当一个句子是可满足的，它将返回一个生成该句子的模型 True . 如果不能满足，它就会回来 False .

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

检查命题句的可满足性。成功时返回模型。对于微不足道的真表达式，返回{true:true}。

在将所有的模型设置为True时，如果给定的表达式是可满足的，则返回一个模型生成器。但是，如果expr不可满足，则返回包含单个元素False的生成器。

实例

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