我在一个项目中工作，我必须在 CNF 表格中生成命题公式来执行一些测试；我遇到了以下问题：
对于第二个问题我有一个想法，例如我们可以生成一个随机公式p，然后取公式p or not p，然后将生成的公式转换为CNF，但问题是我们能否生成所有有效的公式这边？
这里允许的布尔运算符是：or,and,not
感谢您的帮助
【问题讨论】：
标签： algorithm logic theory boolean-logic
首先，让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, @987654339 @ 和 ni 的，你必须能够有效地计算哪些公式是可满足的（从而隐式解决 3-SAT 问题）。出于这个原因，我相信没有多项式时间算法（除非 P=NP）来生成 random 3-CNF（这样每个可满足具有给定结构的 3-CNF 同样可能）。因为生成随机 3-CNF 很困难，所以生成 CNF 一般也是如此。
可能有一些算法可以生成可满足的 3-CNF 子集，这对于实际目的可能已经足够了；生成不可满足的实例也是如此。
【讨论】：
p or not p 中指出的那样，随机 p 是那些子集之一满意，但我不知道是否存在其他处理问题的方法