我在一个项目中工作，在这个项目中我必须生成 CNF 形式的命题公式来执行一些测试；我遇到了以下问题:
- 如何生成随机可满足公式？
- 如何生成随机有效公式？
对于第二个问题我有一个想法，比如我们可以生成一个随机的公式p然后取公式p or not p然后转换得到的公式在 CNF 中，但问题是我们可以通过这种方式生成所有有效的公式吗？
此处允许的 bool 运算符是:or,and,not
谢谢你的帮助
最佳答案
首先，让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 的子集的算法，这对于实际目的来说可能已经足够好了；生成不可满足的实例也是如此。
关于algorithm - 生成可满足和不可满足的公式，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/36405616/