python - 从布尔表达式生成 CNF

Question

具体问题

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

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

ATMOST_1 (( A1 and not (A11, A12, A13, ...)) or (A2 and not (A21, A22, ...) or ... )) and
ATMOST_1 (( B1 and not (B11, B12, B13, ...)) or (B2 and not (B21, B22, ...) or ... )) and
ATMOST_1 ( ... )

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

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

目标问题

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

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

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

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

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

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

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

这给出了以下布尔公式：

( cell1_var1 & ~{constraints} | cell1_var2 & ~{constraints} | ... ) &
( cell2_var1 & ~{constraints} | cell2_var2 & ~{constraints} | ... ) &
... (until there are no blank cells)

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

cell1_var1 & ~{constraints}
cell1_var2 & ~{constraints}
...

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

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

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

SAT的注意事项

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

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

标签： pythonbooleansatcnf