有没有一个好的算法可以在没有额外变量的情况下对 CNF 进行最小计算？

Is there a good algorithm for the minimal computation of a CNF without extra variables?

提问人：Felix Rausch 提问时间：2/1/2023 更新时间：2/2/2023 访问量：80

问：

我目前正在研究将数据库系统的逻辑查询从 DNF 形式转换为 CNF 形式，重点是具有类似形式的查询， 到(a and b and c and d and e1) or (a and b and c and d and e2) or (a and b and c and d and e3)a and b and c and d and (e1 or e2 or e3)

我预计已经有一种算法可以做到这一点，但我目前正在使用 z3，从中看到的形成 CNF 的唯一方法是使用 tseitin 或类似的东西，其中包括额外的变量，这是一个问题，因为它们不能正确地用于查询。

数据库 z3 布尔逻辑

评论

0赞 alias 2/1/2023
您可以，但翻译可以产生指数级更大的公式。但是，如果您的示例足够小，那么这也许没什么大不了的。
0赞 Felix Rausch 2/1/2023
它主要用于与示例相似的公式，不同部分的逻辑重叠很大。我遇到的问题是在运行时减小大小，以便不会一次计算所有内容，而是减少计算的选项数量。
0赞 alias 2/1/2023
让 SAT/SMT 求解器完成其工作。不要担心“计算一切”。SAT/SMT 搜索的全部意义在于进行智能搜索以获得您满意的集合。除非你观察到巨大的减速，否则我根本不会担心这一点。（如果你这样做了，那么你应该发布一个让你很难的示例查询。
0赞 Felix Rausch 2/2/2023
我需要这个数据库系统。我找不到一个满意的集合是没有用的。我需要一个可以拆分并向下推查询图的结合公式。
0赞 alias 2/2/2023
那么，您正在使用 z3 将 dnf 转换为 cnf？没有任何实际的解决方案？

答：

0赞 alias 2/2/2023 #1

为此目的使用 z3 可能不是最佳选择。虽然有一个内部转换器，但它经过调整后可以与求解器的其余部分结合使用。如果您不需要找到令人满意的模型，则不应使用 SAT/SMT 求解器。

从DNF到CNF的转换可以产生指数级的大公式，这就是为什么大多数实际应用都会使用Tseytin变换来降低这种复杂性的原因;这增加了额外的变量。如果您不希望这样做，则应使用 Quine-McCluskey 算法，该算法具有最坏情况的指数行为。但是，如果您的公式足够小，可以开始，这可能无关紧要。

你可以自己编写这个算法，或者如果你愿意使用 SymPy，有一个现有的实现（可能进行简化）。查看 https://docs.sympy.org/latest/modules/logic.html?highlight=to_cnf#sympy.logic.boolalg.to_cnf

评论

0赞 Felix Rausch 2/2/2023
我不认为这就是我要找的。理想情况下，我需要的算法不应该花这么长时间，而是在我的示例中更加线性。例如，在我的示例中，即使我在三个子句中添加了 f、g、h、...、z 等，它也应该只随着变量的数量而增长多项式。（我认为在这种情况下，它甚至可以在线性时间内工作）。
0赞 alias 2/2/2023
一般的CNF转换是昂贵的。但是，如果您的输入是某种样式，它可能会工作得更快。请注意，这不会改变您应该使用的算法：您只会在效果良好的地方使用它。

上一个：如何减少 for 循环的数量？

下一个：字节屏蔽 AxiStream：如何使用 tkeep systemverilog 屏蔽 tdata