1

我目前正在尝试使用 SAT 求解器来解决难题“Kuromasu”，该求解器采用常见的 DIMACS 格式，即作为连接范式 (CNF) 的输入。

在 Kuromasu 中，您有一个带有 mxn 单元的矩形板。一个细胞要么是黑色的，要么是白色的。游戏的目标是决定哪个单元格是哪种颜色。一些单元格包含一个数字。包含数字的单元格始终为白色。该数字告诉您应该从该单元格中看到多少个单元格，包括其自身。同一行和同一列中的所有白色单元格都是可见的，直到第一个黑色单元格。

示例 5x4 网格，# 表示黑色单元格：

___________ 
| | |#| |2|   <-- 2 cells including itself visible
___________
| | |#| |#|
___________ 
| |#|3| |#|   <-- 3 cells including itself visible
___________ 
| | | | | | 
___________

我需要制定这个约束，以 SAT 求解器理解的方式找到黑色区域的位置。我已经能够通过遍历编号单元格左侧、右侧、顶部、底部的所有单元格并检查将它们着色为黑色是否满足约束来为每个数字生成一个分离范式 (DNF) 版本。这给了我一份 DNF 中可能的黑细胞星座列表。我通过在每个单元格中引入一个变量来对游戏进行编码，如果为假，则为黑色，如果为真，则单元格为白色。以下是上述字段的所有变量（1 索引，因为 DIMACS 格式将假变量指定为负整数，将真变量指定为正对应）：

________________ 
| 1| 2| 3| 4| 5|   
________________
| 6| 7| 8| 9|10|
________________ 
|11|12|13|14|15|   
________________
|..|..|  |  |  | 
________________

仅对于上面示例中的 2-number 约束，我将生成以下内容：

___________ 
| | | | |2|   <-- 2 cells including itself visible
___________
| | | | | |
___________ 
| | | | | |   
___________ 
| | | | | | 
___________

(-4 & -15) | (-3 & -10) (等式 1.)

这代表了可以遵循约束的两种方式。但是，要将其输入到 SAT-Solver，我需要将 (Eq 1.) 转换为 CNF。我实现了一个（简单的）转换器，它可以工作，但由于转换为 CNF的复杂性，它确实很慢且内存密集。对于有超过 4 种方式来实现它们的约束，这样做是不可行的。

如何以可以直接提供给 Solver 的方式制定约束？可能吗？这个问题我想了好久，还是搞不明白。

谢谢！

4

1 回答 1

1

上面评论中提到的 Tseytin 变换效果很好。这是java中的一些代码，以防其他人需要它。

请注意：这不是 Tseytin 变换的完整实现，它仅在输入已经在 DNF 中时才有效。下面的代码也只是一个 hacky 解决方案的示例，例如，输入和输出本质上是相同的格式，只是不同的解释，这不是很安全。随意根据需要进行修改。

编辑：为了我自己的安全/学术诚实，一旦完成截止日期的课程作业结束（1 月 8 日），我将添加代码。

于 2016-12-27T16:44:21.017 回答