用Python从逻辑表中创建Dnf和Cnf（sympy，sagemath）

Question

如果有人知道的话，我目前正在OpenEDX中开发任务。 我想创建logictables，让其他人从logictable中评估dnf和cnf。 我开始使用Symphy，但它只评估一个答案，所以我发现了sagemath，它也有一个逻辑库。 所以我尝试了一下，但我不确定如何手动创建一个logictable并从中获取dnf。在文档中，您可以从逻辑函数中获取truthtable，还是我遗漏了什么

s = propcalc.formula("z1")
s.truthtable()

我希望我可以用这样的东西手动生成一个truthtable

t = logictable.truthtable(values, variables)

把dnf弄出来

Answer 1

要创建真值表，请使用sympy.satisfiable函数，列出所有 使逻辑表达式为真的符号赋值

使用此真值表，sympy.POSform和sympy.SOPform函数 将提供最小的POS或SOP逻辑表达式

另外，请注意sympy.sympify使用eval，因此请确保字符串表达式 已经消毒了

from sympy import *

my_names = 'ABCD'
A,B,C,D = symbols(','.join(my_names))
ns1 = {'A': A, 'B': B, 'C': C, 'D': D}
my_symbols = tuple(ns1.values())
es1 = '~(C | D | ~(A | B))'
e1 = sympify(es1, locals=ns1)
print(f"String {es1} with symbols {my_symbols}",
      f"\n\tmakes expression {e1}")
models = satisfiable(e1, all_models=True)
minterms = list(models)
print('SOP form (DNF):', SOPform(my_symbols, minterms))
print('POS form (CNF):', POSform(my_symbols, minterms))

输出：

# String ~(C | D | ~(A | B)) with symbols (A, B, C, D)
#   makes expression ~(C | D | ~(A | B))
# SOP form (DNF): (A & ~C & ~D) | (B & ~C & ~D)
# POS form (CNF): ~C & ~D & (A | B)