问题标签 [cnf]

输入是 2-CNF 中的布尔公式，以符号字符串的形式给出。

示例：p /\ (p -> q) /\ (p -> ~r) /\ (~r / ~s) /\ (s / ~q)

我正在使用解决方法来解决这个 2 cnf sat 问题，但我被困在如何比较 python 中两个子句的文字，因为我们需要在另一个子句中检查变量及其否定

具体问题

我有一个问题，我想在 Python 中使用SAT求解器（例如pycosat或cryptominisat）来解决。SAT 求解器接受问题输入作为由单个布尔子句组成的CNF 表达式列表。

对于我的具体任务，问题可以表示为以下布尔伪代码：

在这里，ATMOST_1意味着一个约束告诉只有 0 或 1 个共轭表达式 (A1, A2, ...) 必须为真。

我不明白如何将其转换为有效的 CNF。为了更好地理解这个问题的根源，请进一步阅读......

目标问题

根本问题是我正在研究的自动 Arroword 填充算法。Arroword 是一个填字游戏类型的谜题，其中被阻塞的单元格包含相邻单词的线索。这是一个 25x25 Arroword 网格的示例，其中显示了各种单词/线索对（单词单元格为绿色，线索单元格选项为橙色）：

这个网格的垂直和水平单词/线索选项的总数是 28248（我做了一个相当长的公式来从网格大小和最小/最大字长得出这个数字）。因此，在 SAT 术语中，它意味着完全相同的变量。

为了解决 SAT 问题，我们还需要添加约束。自然地，每个单词/线索变体都有其基于其位置、长度和结构的约束。下面是一个示意图，显示给定单词的约束：

此处的约束以灰色突出显示的单元格显示。基本上对于每个单词/线索（变量），都适用以下约束：

• 没有其他词可以从同一个线索单元中追踪到
• 没有与给定单词在同一方向上重叠的单词（“扩展”它）
• 没有词穿过线索单元（在任何方向）

在实践中，每一个这样的约束都是满足上述标准的变量池的一个子集。所以在这里我们处理有问题的SAT问题：

对于网格中的每个单元格，找到满足其约束的 0 或 1 个变量（“最多 1 个”）。

这给出了以下布尔公式：

在 DNF 格式中，它看起来要简单得多，例如：

最终的任务是最大化令人满意的条款的数量。

我的代码目前可以生成变量池（如果需要，将它们编码为整数），以及每个变量的约束。

在选择 SAT 解决方案时，我受到了SO 上的这篇文章的启发。事实上，这是一个非常接近我自己的解决方案，但是，它对我的​​理解来说太硬核了......

SAT的注意事项

在处理问题时我想实现的一些事情：

• 制作一个单独的子句来监控未填充（空白）单元格的数量（没有单元格必须留空） - 增量解决可能会有所帮助？
• 从 DNF/混合类型公式转换时避免 CNF 子句的多项式扩展（订单的可变计数为 10k 并且每个约束约 1k，它可能会产生数十亿条线索）

我有一个解决方案，它对CNF公式中的子句数量具有线性时间复杂度，即O（c ^ 2 X n），使得n是CNF公式中不同变量的数量，是否会考虑这个解决方案是否作为 K-CNF 的线性解？由于子句的数量可能是 c = 2^n 算法应该使其线性以解决 K-CNF 的实变量是多少？可以是C吗？或者应该是n？或者是什么？

我没有正确理解 CNF 复杂性问题