from sympy import symbols, satisfiable, simplify_logic, true, false, And, Or, Not
from sympy.logic.boolalg import ANFform, truth_table, BooleanTrue, to_cnf, to_dnf
# Sum Of Production Form积和式, Production of Sum Form和积式
from sympy.logic import SOPform, POSform 
import numpy as np
from itertools import combinations
# 逻辑运算符：~否定，&合取，|析取，!=异或，>>蕴含，==等价
# 定义符号变量
p, q, r = symbols('p q r')
# 定义命题逻辑表达式
exp = (p | q >> r) >> p
# 用真值表法输出表达式的所有值
table = truth_table(exp, [p, q, r])
print('真值表')
print('p q r -> exp')
print('-' * 15)
for t in table:
    [pv, qv, rv], rst = t
    print(pv, qv, rv, '->', int(rst == true))
# 判断表达式的可满足性并求解
print('逻辑表达式可满足性判别并求解')
models = satisfiable(exp, all_models=True)
if models:
    rst = list(models)
    data = []
    varNames = []
    for dv in rst:
        if len(varNames) == 0:
            varNames = list(dv.keys())
        data.append([int(v) for v in list(dv.values())])
        #rst.append([dv[p], dv[q], dv[r]])
    print([ch for ch in varNames])
    print('-' * 15)
    data = np.array(data, int)    
    print(data)
# 获取表达式的合取范式和析取范式（非标准）    
# conjunctive normal form 和 disjunctive normal form
print('合取范式cnf=', simplify_logic(exp, 'cnf'))
print('析取范式dnf=', simplify_logic(exp, 'dnf'))
print('合取范式cnf=', to_cnf(exp))
print('析取范式dnf=', to_dnf(exp))
# 由随机真值表确定响应的真值函数——决策函数
# 动态定义4个变量——A,B,C,D
nVars = 4
vars = [chr(97 + i) for i in range(nVars)]
code = ','.join(vars) + " = symbols('" + ' '.join(vars) + "')"
print('code=', code)
exec(code)      #运行生成的代码code，以动态创建变量
# 生成变量的2 ** nVars个01的值组合
tbl = []
for i in range(2**nVars):
    bins = bin(i)[2:]
    bins = '0' * (nVars - len(bins)) + bins
    bins = [int(v) for v in bins]
    tbl.append(bins)
tbl = np.array(tbl, int)
# 随机生成y值表，并记录值为True的行号
yTrueIdx = [i for i, v in enumerate(np.random.randint(0, 2, (2 ** nVars))) if v == 1]
# 由真值表获得对应的赋值项
minterms = []
for rowno in yTrueIdx:
    minterms.append(list(tbl[rowno, :]))
print('最小项', minterms)
dontcares = []  #不关心项
# 取得由真值表所确定的真值决策函数表达式字符串
f1 = SOPform(vars, minterms, dontcares) #积和式
print('函数SOP形=', f1)
f2 = POSform(eval(','.join(vars)), minterms, dontcares) #积和式
print('函数POS形=', f2)
# 把变量名转换为数组索引
f3 = str(f1)
# 把f3中的个体变量名都更新为xs的数组下标表示
for i, var in enumerate(vars):
    f3 = f3.replace(vars[i], 'xs[%d]' % (i))
# 注意：由于sympy中的~逻辑运算在python中是位运算，故~-1=-2，导致不是严密的逻辑运算    
# 因此，需要把sympy中的逻辑运算符替换为python语言的逻辑运算符
f3 = f3.replace('~', ' not ')    
f3 = f3.replace('&', ' and ')    
f3 = f3.replace('|', ' or ')    
print('数组表示的f3=', f3)    
# 由f3结合lambda表达式以动态创建函数 
# f3= (xs[1]  and  xs[3]  and   not xs[2])  or  (xs[3]  and   not xs[0]  and   not xs[2])  or  (xs[1]  and  xs[2]  and   not xs[0]  and   not xs[3])
F3 = eval('lambda  xs : ' + str(f3))
# 把minterms中的项代入计算，检查是否不等于0
for no, row in enumerate(tbl):    
    value = True if no in yTrueIdx else False
    val = F3(row)
    print(no, row, int(value), int(val), 'Ok' if int(value) == int(val) else 'Err')

运行结果：

真值表
p q r -> exp
---------------
0 0 0 -> 0
0 0 1 -> 0
0 1 0 -> 1
0 1 1 -> 0
1 0 0 -> 1
1 0 1 -> 1
1 1 0 -> 1
1 1 1 -> 1
逻辑表达式可满足性判别并求解
[r, p, q]
---------------
[[0 1 1]
[0 1 0]
[0 0 1]
[1 1 1]
[1 1 0]]
合取范式cnf= (p | q) & (p | ~r)
析取范式dnf= p | (q & ~r)
合取范式cnf= (p | q) & (p | ~p) & (p | ~r)
析取范式dnf= p | (q & ~p & ~r)
code= a,b,c,d = symbols('a b c d')
最小项 [[0, 0, 0, 0], [0, 0, 0, 1], [0, 0, 1, 0], [0, 0, 1, 1], [0, 1, 0, 1], [0, 1, 1, 0], [1, 0, 1, 0], [1, 1, 0, 1]]
函数SOP形= (~a & ~b) | (b & d & ~c) | (c & ~a & ~d) | (c & ~b & ~d)
函数POS形= (b | c | ~a) & (c | d | ~b) & (b | ~a | ~d) & (d | ~a | ~b) & (~b | ~c | ~d)
数组表示的f3= ( not xs[0]  and   not xs[1])  or  (xs[1]  and  xs[3]  and   not xs[2])  or  (xs[2]  and   not xs[0]  and   not xs[3])  or  (xs[2]  and   not xs[1]  and   not xs[3])
0 [0 0 0 0] 1 1 Ok
1 [0 0 0 1] 1 1 Ok
2 [0 0 1 0] 1 1 Ok
3 [0 0 1 1] 1 1 Ok
4 [0 1 0 0] 0 0 Ok
5 [0 1 0 1] 1 1 Ok
6 [0 1 1 0] 1 1 Ok
7 [0 1 1 1] 0 0 Ok
8 [1 0 0 0] 0 0 Ok
9 [1 0 0 1] 0 0 Ok
10 [1 0 1 0] 1 1 Ok
11 [1 0 1 1] 0 0 Ok
12 [1 1 0 0] 0 0 Ok
13 [1 1 0 1] 1 1 Ok
14 [1 1 1 0] 0 0 Ok
15 [1 1 1 1] 0 0 Ok

使用sympy实施命题逻辑变量的定义及表达式的可满足性求解；

进一步，随机生成真值表，利用sympy的积和形或和积形表达方式获取对应真值表的决策函数符号表达式（其本质相当于实现了二值分类）——相当于决策表算法；利用这一特性，可对多元特征的选取提供简练选择方法.

方法特点在于简练——进一步用途，需要读者深入思考.

sympy 2jax 将 SymPy 表达式 转换为参数化，可微分，可矢量化的JAX 函数 。 所有 SymPy 浮点数都将成为可训练的输入参数。 SymPy 符号成为传递矩阵的列。 pip install git+https://github.com/MilesCranmer/ sympy 2jax.git import sympy from sympy import symbols import jax import jax . numpy as jnp from jax import random from sympy 2jax import sympy 2jax 让我们在 SymPy 中 创建一个 表达式 ： x , y = symbols ( 'x y' ) expression = 1.0 * sympy . cos ( x ) + 3.2 * y 让我们 获取 JAX版本。 我们传递方程式和所 文章目录 合取 范式（ conjunctive normal form (CNF)） 析取范式 （disjunctive normal form (DNF)）简化的 合取 和 析取范式 标准形式（Canonical form）异或标准形式（xor normal form）二元 决策 图 form （ROBDD）子句标准形式（clause form） 合取 范式（ conjunctive normal form (CNF)） 任何命题公式，最终都能够化成 (A1∨A2)∧(A3∨A4)(A_1 \vee A_2) \wedge ( CNF 是 合取 范式的简称，是可满足问题 中 比较重要的概念。在实际应用 中 ，我们一般将约束写成 CNF 范式的格式，然后通过求解器 Solver 对其进行求解。因此 CNF 可以理解为一种问题约束的表现形式。 本文对 CNF 的基本概念，存储形式，及其应用做一点简要的介绍。 python -m http.server 然后在浏览器 中 打开0.0.0.0:8000。 该网站是在上自动生成的。 这些页面使用分支 中 的GitHub页面提供。 应该对分支进行所有修改。 gh-pages分支是自动生成的。 请注意， sources分支根目录 中 的所有文件都同步到gh-pages分支。 如果要添加未翻译的其他文件，则可以在此处添加它们。 但是请考虑： 任何包含内容的页面都应添加到templates以便可以对其进行翻译。 任何图像都应添加到media 。 Python 中 的 Sympy 详细使用 遇到复杂 计算 找 python 绝对不让你失望， sympy 是一个 Python 的科学 计算 库，用一套强大的符号 计算 体系完成诸如多项式求值、求极限、解方程、求积分、微分方程、级数展开、矩阵运算等等 计算 问题。虽然Matlab的类似科学 计算 能力也很强大，但是 Python 以其语法简单、易上手、异常丰富... Sympy 是一个符号 计算 的 Python 库。它的目标是成为一个全功能的 计算 机代数系统，同 时 保持代码简洁、易于理解和扩展。它完全由 Python 写成，不依赖于外部库。 SymPy 支持符号 计算 、高精度 计算 、模式匹配、绘图、解方程、微积分、 组合 数学、离散 数学、几何学、概率与统计、物理学等方面的功能。官方在线文档：Welcome to SymPy ’s documentation! sympy 库安装：pip3 i...