我当前正在尝试用SAT求解器解决拼图" kuromasu"，该求解器以公共DIMAC格式输入，即作为连接的正常形式（CNF）。
在Kuromasu中，您有一个带有MXN细胞的矩形板。细胞是黑色或白色。游戏的目标是确定哪种颜色是哪种颜色。一些单元包含一个数字。包含一个数字的单元格总是白色的。该数字告诉您，该单元格应该可以看到多少个单元格。同一排和色谱柱中的所有白细胞都可以看到，直至第一个黑细胞。
示例5x4网格，＃代表黑细胞：
___________
| | |#| |2| <-- 2 cells including itself visible
___________
| | |#| |#|
___________
| |#|3| |#| <-- 3 cells including itself visible
___________
| | | | | |
___________
我需要以SAT求解器理解的方式来制定此约束以找到黑色场的位置。我已经能够通过通过所有单元格向左，右，顶部，底部，并检查将其涂成黑色是否满足约束，从而可以通过跨，右，顶部，底部的所有单元格生成每个数字的析取常态形式（DNF）的版本。这为我提供了DNF中黑细胞可能存在的星座的列表。我通过引入每个单元格的变量来编码游戏，如果它是错误的，则是黑色的，如果是真实的，则单元格为白色。以下是上面字段的所有变量（1个索引，因为DIMAC格式将false变量指定为负整数，而真实变量为正面的对应方）：
________________
| 1| 2| 3| 4| 5|
________________
| 6| 7| 8| 9|10|
________________
|11|12|13|14|15|
________________
|..|..| | | |
________________
对于上面示例的2个数字约束，我将生成以下内容：
___________
| | | | |2| <-- 2 cells including itself visible
___________
| | | | | |
___________
| | | | | |
___________
| | | | | |
___________
（-4＆amp; -15）|（-3＆amp; -10）（eq 1。）
这表示可以遵循约束的两种方式。但是，要将其输入到SAT-Solver，我需要将（EQ 1.）转换为CNF。我实施了一个（天真的）转换器，该转换器起作用，但由于转换为CNF的复杂性，它确实非常缓慢且内存密集。对于拥有超过4种实现它们的方式的约束，这样做是不可行的。
如何以直接输送给求解器的方式制定约束？是否可以？我已经考虑了一段时间了，而且无法完全理解。
谢谢！
上面评论中提到的tseytin变换效果很好。这是Java中的一些代码，以防其他人需要它。
请注意：这不是tseytin变换的完整实现，如果输入已经在DNF中，则可以工作。下面的代码也只是一个示例hacky解决方案，例如将输入和输出本质上的格式（仅是不同的解释）本质上是相同的格式不是很安全的。可以随时修改。
edit ：为了我自己的安全/学术诚实，我将添加代码，一旦将到期日结束的课程分配（1月8日）。