algorithm - 生成可满足和不可满足的公式

Question

我在一个项目中工作，在这个项目中我必须生成 CNF 形式的命题公式来执行一些测试；我遇到了以下问题:

1. 如何生成随机可满足公式？
2. 如何生成随机有效公式？

对于第二个问题我有一个想法，比如我们可以生成一个随机的公式p然后取公式p or not p然后转换得到的公式在 CNF 中，但问题是我们可以通过这种方式生成所有有效的公式吗？

此处允许的 bool 运算符是:or,and,not

谢谢你的帮助

Answer 1

首先，让L是 k 的集合文字 l1,l2,l3,...,lk对于预先指定的 k .现在给定一组文字，我们可以从中生成 CNF 公式。

我建议首先选择子句的数量——即组合的 OR 表达式的数量---，比如说 m , 然后 n_1 , n_2 ,..., n_m , 其中n_i是 OR 连接文字的数量。您可以随机选择这些数字，也可以将它们作为参数以更好地控制公式的大小和结构。

例如，对于 m=2和 n1=2和 n2=2你会有 (l1 OR l2) AND (l3 OR l4) 形式的 CNF其中 li的选自 L并且是否被否定。

现在您知道公式的样子了，遍历文字的位置并针对每个位置:

• 选择文字 l来自 L均匀随机；
• 掷一枚公平的硬币来决定是否否定文字。

您最终得到了 CNF 中的“随机”公式。但是，您不知道它是否可满足。

更新(2016 年 4 月 5 日)。如果您想使用给定参数有效生成随机可满足的 CNF k , m , 和 ni的，您必须能够有效地计算出哪些公式是可满足的(从而隐含地解决了 3-SAT 问题)。出于这个原因，我相信没有多项式时间算法(除非 P=NP)用于生成随机 3-CNF(以便每个可满足的具有给定结构的 3-CNF 同样可能)。因为生成随机 3-CNF 很困难，所以一般生成 CNF 也很困难。

可能存在用于生成可满足的 3-CNF 的子集的算法，这对于实际目的来说可能已经足够好了；生成不可满足的实例也是如此。