SymPy 逻辑模块（sympy.logic）完全指南：从布尔表达式构造到 SAT 求解

SymPy 逻辑模块（sympy.logic）完全指南：从布尔表达式构造到 SAT 求解

【免费下载链接】sympyA computer algebra system written in pure Python项目地址: https://gitcode.com/GitHub_Trending/sy/sympy

导读

SymPy 的sympy.logic模块提供了一套完整的命题逻辑（propositional logic）工具箱：你既可以用&、|、~等 Python 运算符直接构造和操作符号化布尔表达式，也可以借助SOPform、POSform、ANFform从真值表反推逻辑函数，还能通过to_cnf/to_dnf等函数完成范式转换、使用simplify_logic化简，并最终用satisfiable、valid、entails等推理例程进行可满足性判定与知识库推理。读完本文，你将掌握这一模块从表达式构造、范式变换、真值表映射到 SAT 求解的完整调用链，并了解其背后的源码实现（主要位于 sympy/logic/boolalg.py 与 sympy/logic/inference.py）。

构造逻辑表达式

使用 Python 运算符直接构造

逻辑模块的核心能力是"用 Python 原生运算符表达逻辑运算"。所有标准布尔运算符都被重载在 Boolean 基类上，与直觉完全一致：

• &→And（合取，逻辑与）
• |→Or（析取，逻辑或）
• ~→Not（否定，逻辑非）
• >>→Implies（蕴含x >> y表示Implies(x, y)）
• <<→Implies（反向蕴含，x << y表示Implies(y, x)）
• ^→Xor（异或）

文档给出的基础示例可以直接在交互环境中验证：

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

从源码看，运算符重载的实现位于Boolean基类，例如__and__直接返回And(self, other)，__rshift__返回Implies(self, other)，__lshift__返回Implies(other, self)（见 boolalg.py）。__or__、__xor__、__invert__同理，且都定义了对应的反向运算符（__rand__、__ror__等），因此True & x这类 Python 布尔值与符号混合的写法也能正常工作。

与 SymPy 基础框架的集成

与 SymPy 中大多数类型一样，布尔表达式继承自Basic，因此天然具备subs替换、atoms原子提取等能力：

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

subs在 Boolean 中被重载，返回类型标注为Boolean，保证替换后的结果仍是布尔对象。此外Boolean还提供了equals（真值表等价判断，见 boolalg.py）、as_set（把布尔表达式改写为实数集，如Eq(x, 0).as_set()返回{0}）等高级方法。

布尔函数类总览

逻辑模块内置了完整的布尔函数类型，全部定义在 sympy/logic/boolalg.py 中。文档通过 autoclass 指令收录了以下核心类：

一个与gateinputcount（见下文）相关的细节值得注意：Nand、Nor、Xnor默认会展开成Not(And(...))等形式，这会影响门输入计数，测试用例可在 sympy/logic/tests/test_boolalg.py（如test_Nand、test_Xnor）中找到验证。

由真值表推导逻辑函数：SOPform / POSform / ANFform

这是逻辑模块最有实用价值的功能之一：给出输出为 1 的输入组合（minterms，最小项），自动生成最简的逻辑表达式。

SOPform：和之积（最小项之和）

SOPform(variables, minterms, dontcares=None)使用简化的成对比较（_simplified_pairs）加冗余组消除算法（_rem_redundancy），把生成1的输入组合转换为最小的"和之积"（sum-of-products）形式，返回Or对象。其实现见 boolalg.py。

>>> 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与dontcares支持三种等价表示，源码通过_input_to_binlist统一归一化（见 boolalg.py）：

• 二进制列表：如[[0, 0, 0, 1], ...]，按variables顺序逐位给出；
• 整数：如[1, 3, 7, 11, 15]，整数即二进制位的十进制表示；
• 字典（允许部分指定）：如[{w: 0, x: 1}, {y: 1, z: 1, x: 0}]。

三种写法可混用，例如：

>>> 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：和之积（最大项之积）

POSform与SOPform输入完全一致，但输出的是"积之和"（product-of-sums）形式，返回And对象。内部实现先把未出现在 minterms 与 dontcares 中的组合作为 maxterms（最大项），再对 maxterms + dontcares 做同样的化简（见 boolalg.py）。

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

注意：SOPform 与 POSform 使用 Quine-McCluskey 算法（源码 docstring 明确引用了该算法与 don't-care 术语），结果是最简形式之一，但可能不是唯一解——文档原文明确提示"The result will be one of the (perhaps many) functions that satisfy the conditions"。此外，若某个 minterm 同时出现在 dontcares 中，函数会抛出ValueError。

ANFform：代数范式（Zhegalkin 多项式）

ANFform(variables, truthvalues)把真值表的结果列转换为代数范式（Algebraic Normal Form，即 Zhegalkin 多项式）。在这种表示中，True对应 1、False对应 0，And即乘法、Xor即加法：

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

实现上，ANFform先调用anf_coeffs(truthvalues)得到 Zhegalkin 系数，再对系数为 1 的项用_convert_to_varsANF转换为变量合取，最后组装成Xor（见 boolalg.py）。若truthvalues长度不等于2^n（n 为变量数），会抛出ValueError。

范式转换：ANF / CNF / DNF / NNF

逻辑模块提供了四套"范式"的转换与判定函数，全部位于 sympy/logic/boolalg.py：

to_cnf与to_dnf的行为高度对称，源码实现的关键点在于：

• 若表达式已是目标范式则直接返回，不做多余转换（"Don't convert unless we have to"，见 boolalg.py）；
• 先eliminate_implications(expr, form=...)消除蕴含，再做分配律展开；
• 当simplify=True时，内部走simplify_logic(expr, 'cnf'/'dnf', True, force=force)，使用 Quine-McCluskey 求最简形式，可能非常耗时；当变量超过 8 个时，必须显式传force=True，否则抛出ValueError（见 boolalg.py）。

示例：

>>> from sympy.logic.boolalg import to_cnf, to_dnf, to_nnf, to_anf >>> from sympy.abc import A, B, C, D >>> to_cnf(~(A | B) | D) (D | ~A) & (D | ~B) >>> to_cnf((A | B) & (A | ~A), True) # simplify=True A | B >>> to_dnf(B & (A | C)) (A & B) | (B & C) >>> to_nnf(Not((~A & ~B) | (C & D))) (A | B) & (~C | ~D) >>> to_anf(Not(A)) A ^ True

关于 ANF 的一个关键特性：它是规范范式（canonical normal form）——两个等价的公式转换后必然得到相同的 ANF（见 boolalg.py），因此可用于公式等价性判定。

化简与等价性测试

simplify_logic：最简 SOP/POS 化简

simplify_logic(expr, form=None, deep=True, force=False, dontcare=None)把布尔函数化简为最简 SOP 或 POS 形式，返回值是Or或And对象。核心参数（见 boolalg.py）：

• form：'cnf'或'dnf'时返回对应范式的最简表达式；None（默认）时返回参数个数更少的形式（默认偏向 CNF）；
• deep：是否递归化简输入中内嵌的非布尔函数（如关系式）；
• force：默认限制 8 个变量以内才做完整化简，超过 8 个变量只做符号级化简（由deep控制）；force=True解除限制但可能耗时极长；
• dontcare：指定在该表达式为真的输入视为无关项（don't care），典型场景是Piecewise的条件化简——先前条件已经覆盖的输入无需再考虑。

示例：

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

simplify_logic的内部实现相当精巧：先把关系式（Relational）替换为Dummy符号以减少变量数、再生成真值表并用_get_truthtable计算、最后套用模式库_simplify_patterns_and/_simplify_patterns_or/_simplify_patterns_xor进行模式化化简（见 boolalg.py）。同时，SymPy 的通用 simplify 函数也可以化简逻辑表达式到最简形式，这是文档明确提示的另一条路径。

bool_map：变量重命名下的逻辑等价

bool_map(bool1, bool2)判断两个布尔表达式是否在某种变量对应关系下逻辑等价：若存在这样的映射，返回(化简后的bool1, 变量映射字典)；否则返回False（见 boolalg.py）。

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

实现分两步：先对两个表达式分别simplify_logic，再用指纹字典（_finger）做结构匹配（内部match函数）。文档也提醒：映射结果不唯一但规范（canonical）——例如(w, z)可能对应(a, d)也可能对应(d, a)，函数只保证返回其中之一。针对指纹匹配的健壮性问题（如 issue 4835 描述的Basic.match缺陷），代码注释说明这是一种专门为化简后布尔表达式设计的替代方案。

表达式操作

逻辑模块还提供一组直接操作表达式结构的函数（见 boolalg.py）：

• distribute_and_over_or(expr)：把合取分配到析取上，得到 CNF。Or(A, And(Not(B), Not(C)))→(A | ~B) & (A | ~C)；
• distribute_or_over_and(expr)：把析取分配到合取上，得到 DNF，输出不做化简。And(Or(Not(A), B), C)→(B & C) | (C & ~A)；
• distribute_xor_over_and(expr)：把异或分配到合取上，输出不做化简。And(Xor(Not(A), B), C)→(B & C) ^ (C & ~A)；
• eliminate_implications(expr, form=None)：消除蕴含与等价，转换为等价的 NNF（内部直接调用to_nnf(expr, simplify=False, form=form)，见 boolalg.py）。例如Equivalent(A, B, C)→(A | ~C) & (B | ~A) & (C | ~B)。

这三个distribute_*函数共用底层递归分发器_distribute，其逻辑是：若表达式是指定外层运算符的实例且参数中存在另一运算符，则把该参数逐个与其余部分组合并递归分发（见 boolalg.py）。

真值表与整数表示映射

truth_table：生成真值表

truth_table(expr, variables, input=True)返回一个生成器，产出所有输入组合及其对应的表达式取值。核心参数：

• expr：待求值的布尔表达式；
• variables：变量列表（注意：真值表按product((0, 1), repeat=len(variables))全排列，变量顺序影响输出顺序）；
• input：True时产出(输入列表, 结果)元组；False时只产出结果值序列。

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

当input=False时，输出序列的下标对应输入组合的二进制编码，可与sympy.utilities.iterables.ibin配合还原输入（文档给出了[(y, 0), (x, 0)] -> True的完整还原示例，见 boolalg.py）。

整数 / 项 / 符号之间的映射

这一组函数解决"真值表位置（整数）↔ 0/1 列表 ↔ 符号表达式"之间的互转问题：

其中anf_coeffs通过逐层异或（x^y）的蝶形计算把真值列变换为系数列，bool_monomial与anf_coeffs配合即可从真值表手工重建 Zhegalkin 多项式（源码 docstring 给出了完整示例，见 boolalg.py）。to_int_repr的整数表示是下游 SAT 求解器（见下文）直接使用的内部格式。

推理：satisfiable 与 SAT 求解器

sympy.logic.inference模块（inference.py）实现了命题逻辑的推理例程。文档特别强调了satisfiable：

给定一个布尔表达式，satisfiable判定它是否可满足——即是否存在一组变量赋值使整个句子为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}

返回值约定：可满足时返回一个模型（变量→真值的字典）；不可满足时返回False。这个例子恰好演示了"x & ~x永假，而三子句合取式有模型x=True, y=True"。

satisfiable 的算法选择

satisfiable(expr, algorithm=None, all_models=False, minimal=False, use_lra_theory=False)支持多种后端 SAT 求解器，算法选择逻辑见 inference.py：

• algorithm 参数可选值：'dpll'、'dpll2'、'pycosat'、'minisat22'、'z3'；
• 默认行为：algorithm=None时优先尝试pycosat，若未安装则静默回退到纯 Python 实现的dpll2（同样地，minisat22需要pysat、z3需要z3库，缺失时都回退dpll2）；
• all_models=True：可满足时返回模型生成器（可用next()逐个取出）；不可满足时返回只含单个元素False的生成器；
• minimal=True：要求返回最小模型（仅当使用minisat22后端时有效）；
• use_lra_theory=True：启用线性实数算术理论（Linear Real Arithmetic），此时强制使用dpll2，若显式传入其他 algorithm 会抛ValueError。

纯 Python 的 DPLL 实现位于 sympy/logic/algorithms/dpll.py（经典 DPLL：单元传播unit_propagate、纯符号find_pure_symbol、单元子句find_unit_clause）与 sympy/logic/algorithms/dpll2.py（现代实现，内置 VSIDS 决策启发式与子句学习选项）；外部求解器封装位于 sympy/logic/algorithms/pycosat_wrapper.py、minisat22_wrapper.py、z3_wrapper.py。这些求解器共同的基础是把 CNF 转换为整数表示的子句集（to_int_repr）。satisfiable的all_models、valid、entails等行为在 sympy/logic/tests/test_inference.py 中有系统性测试。

更多推理例程

inference模块还提供：

• valid(expr)：判定表达式是否有效（对所有赋值恒真）。实现为not satisfiable(Not(expr))（见 inference.py）。如valid(A | ~A)为True；
• pl_true(expr, model=None, deep=False)：判断给定赋值是否为该表达式的模型。部分赋值时可能返回None表示"尚不明确"；deep=True时会对剩余部分做有效/可满足性分析，给出更精确的答案（见 inference.py）；
• entails(expr, formula_set=None)：判断子句集是否蕴含某公式；formula_set为空时退化为判定公式的效性。实现为把Not(expr)追加进子句集后检查合取式是否不可满足（见 inference.py）。如entails(C, [A >> B, B >> C, A])为True；
• literal_symbol(literal)：提取文字（literal）对应的符号（去掉否定外层），如literal_symbol(~A)返回A（见 inference.py）。

PropKB：命题知识库

inference模块还提供了知识库框架：抽象基类KB定义tell/ask/retract接口与clauses属性，PropKB(KB)是其命题逻辑实现（见 inference.py）：

• tell(sentence)：把句子的子句加入知识库（内部用conjuncts(to_cnf(sentence))展开为 CNF 子句集合）；
• ask(query)：用entails(query, self.clauses_)判断查询是否为知识库的逻辑结论；
• retract(sentence)：从知识库移除对应子句。

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

类 docstring 明确自述"a KB for Propositional Logic. Inefficient, with no indexing"，即这是一个教学级、无索引的朴素实现，适合理解推理原理。

门电路输入计数：gateinputcount

gateinputcount(expr)返回实现该布尔表达式所需的逻辑门输入总数，常用于数字电路综合与代价估算（见 boolalg.py）。计数规则：

• 只承认标准门：And、Or、Xor、Not、ITE（多路选择器）；Nand、Nor、Xnor会先被展开为Not(And(...))等再计数（evaluate=False可避免展开）；
• 关系比较（如x > z）和符号按一个布尔变量计；单个符号计 0；
• 非布尔输入抛出TypeError。

>>> from sympy.logic import And, Or, Nand, Not, gateinputcount >>> from sympy.abc import x, y, z >>> gateinputcount(And(x, y)) 2 >>> gateinputcount(Or(And(x, y), z)) 4 >>> gateinputcount(Nand(x, y, z)) # 自动展开为 Not(And(x,y,z)) 4 >>> gateinputcount(Nand(x, y, z, evaluate=False)) 3

实用工作流：一个完整示例

把上述能力串起来，一个典型的"真值表 → 最简逻辑 → 可满足性验证"工作流如下：

from sympy import symbols from sympy.logic import SOPform, POSform, simplify_logic from sympy.logic.inference import satisfiable, valid from sympy.logic.boolalg import truth_table, to_cnf w, x, y, z = symbols('w x y z') # 1. 由真值表推导最简 SOP / POS 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]] sop = SOPform([w, x, y, z], minterms, dontcares) # (y & z) | (~w & ~x) pos = POSform([w, x, y, z], minterms, dontcares) # z & (y | ~w) # 2. 范式转换，供 SAT 求解器使用 cnf = to_cnf(sop) # 3. 可满足性与有效性判定 print(satisfiable(sop)) # 一个使表达式为真的模型 print(valid(sop | ~sop)) # True：重言式恒有效

深入阅读

• 逻辑模块核心实现：sympy/logic/boolalg.py
• 推理例程（satisfiable / valid / entails / PropKB）：sympy/logic/inference.py
• DPLL 与 SAT 求解器：目录 sympy/logic/algorithms
• DIMACS CNF 文件加载工具（load/load_file）：sympy/logic/utilities/dimacs.py，测试见 sympy/logic/tests/test_dimacs.py
• 单元测试（覆盖运算符重载、范式转换、bool_map、simplify_logic、求解器回退等）：sympy/logic/tests/test_boolalg.py 与 sympy/logic/tests/test_inference.py
• 本模块与假设系统（assumptions）的联动入口：sympy.logic包导出见 sympy/logic/init.py

总体而言，SymPy 的逻辑模块在纯 Python 环境中同时提供了符号化布尔代数（构造、化简、范式）与命题推理（SAT 判定、知识库）两条能力线：前者面向数字电路设计、真值表综合等场景，后者面向逻辑验证与自动推理。所有核心算法均可脱离外部依赖运行（默认回退到内置的dpll2），而pycosat、pysat、z3等可选后端则按需提供性能增强。

【免费下载链接】sympyA computer algebra system written in pure Python项目地址: https://gitcode.com/GitHub_Trending/sy/sympy