生成可满足和不可满足的公式
Generating satisfiable and non satisfiable formulas
我在一个项目中工作，在这个项目中我必须生成 CNF 形式的命题公式来执行一些测试；我遇到了以下问题：
- 如何生成随机可满足公式？
- 如何生成随机有效公式？
对于第二个问题我有一个想法，例如我们可以生成一个随机公式p然后取公式p or not p然后将得到的公式转换成CNF但问题是我们可以用这种方式生成所有有效的公式吗？
此处允许的布尔运算符是：or,and,not
感谢您的帮助
首先，设 L 为预先指定 k 的 k 个文字 l1,l2,l3,...,lk 的集合。现在给定一组文字，我们可以从中生成 CNF 公式。
我建议首先选择子句的数量——即组合 OR 表达式的数量---，比如 m，然后是 n_1，n_2，...，n_m，其中 n_i 是或连接文字的数量。您可以随意选择这些数字，也可以将它们作为参数以更好地控制公式的大小和结构。
例如，对于 m=2、n1=2 和 n2=2，您将拥有 (l1 OR l2) AND (l3 OR l4) 形式的 CNF，其中 li 选自L 并且是否被否定。
现在您知道公式的样子了，遍历文字的位置，并为每个位置：
- 从
L中随机选择一个文字l；
- 掷一枚硬币决定是否否定文字。
你在 CNF 中得到了一个 "random" 公式。但是，您不知道它是否可满足。
更新（2016 年 4 月 5 日）. 如果你想高效地生成一个 随机 具有给定参数 k、m 和 ni 的可满足 CNF，您必须能够有效地计算哪些公式是可满足的（从而隐式解决 3-SAT 问题).出于这个原因，我相信没有多项式时间算法（除非 P=NP）来生成 random 3-CNF（因此具有给定结构的每个可满足的 3-CNF 都是同样可能的）。因为生成随机 3-CNF 很困难，所以一般生成 CNF 也很困难。
可能存在用于生成可满足的 3-CNF 的子集的算法，这对于实际目的来说可能已经足够好了；生成不可满足的实例也是如此。
我在一个项目中工作，在这个项目中我必须生成 CNF 形式的命题公式来执行一些测试；我遇到了以下问题：
- 如何生成随机可满足公式？
- 如何生成随机有效公式？
对于第二个问题我有一个想法，例如我们可以生成一个随机公式p然后取公式p or not p然后将得到的公式转换成CNF但问题是我们可以用这种方式生成所有有效的公式吗？
此处允许的布尔运算符是：or,and,not
感谢您的帮助
首先，设 L 为预先指定 k 的 k 个文字 l1,l2,l3,...,lk 的集合。现在给定一组文字，我们可以从中生成 CNF 公式。
我建议首先选择子句的数量——即组合 OR 表达式的数量---，比如 m，然后是 n_1，n_2，...，n_m，其中 n_i 是或连接文字的数量。您可以随意选择这些数字，也可以将它们作为参数以更好地控制公式的大小和结构。
例如，对于 m=2、n1=2 和 n2=2，您将拥有 (l1 OR l2) AND (l3 OR l4) 形式的 CNF，其中 li 选自L 并且是否被否定。
现在您知道公式的样子了，遍历文字的位置，并为每个位置：
- 从
L中随机选择一个文字l； - 掷一枚硬币决定是否否定文字。
你在 CNF 中得到了一个 "random" 公式。但是，您不知道它是否可满足。
更新（2016 年 4 月 5 日）. 如果你想高效地生成一个 随机 具有给定参数 k、m 和 ni 的可满足 CNF，您必须能够有效地计算哪些公式是可满足的（从而隐式解决 3-SAT 问题).出于这个原因，我相信没有多项式时间算法（除非 P=NP）来生成 random 3-CNF（因此具有给定结构的每个可满足的 3-CNF 都是同样可能的）。因为生成随机 3-CNF 很困难，所以一般生成 CNF 也很困难。
可能存在用于生成可满足的 3-CNF 的子集的算法，这对于实际目的来说可能已经足够好了；生成不可满足的实例也是如此。