如何将缓慢转换为 CNF 的快捷方式？

编程问答 2022-05-16

问题描述

我正在使用 sympy 来生成这样的表达式：

for crowd in itertools.combinations(symbs,max_true + 1):
    exprs.append(functools.reduce(operator.and_,crowd))
unaltered = ~functools.reduce(operator.or_,exprs)

稍后，我将它们转换为 CNF：

altered = sympy.logic.boolalg.to_cnf(unaltered,simplify=True,force=True)

需要大量的计算机时间。我做了一个包含更多细节的要点：

https://gist.github.com/MatrixManAtYrService/501ea099826a5aeeacc9368710b059ec

鉴于我使用 for 循环生成表达式，它们采用可靠的格式。 Sympy（可以理解）正在做详尽的事情并“手动”解决它们，因为它不知道它们表现得如此好。查看未更改/更改的表达式的人可以轻松确定模式，只需使用 for 循环直接生成 CNF。

在这种情况下这很容易，但我希望有更多的限制。

我想知道我是否处于未知领域，或者只是没有正确地寻求帮助。

Sympy 对这种事情有什么帮助吗？我应该探索另一个图书馆吗？我提议的“查看并根据模式进行推断”策略是否有名称？某处是否有该任务的算法列表？

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

satsympy