我正在尝试使用 SAT 求解器 (sat4j) 实现扫雷求解器，并且我对它们的工作原理有一个简单的了解。但我不知道的一件事是如何表示x+y+Z+....=2地雷，因为 SAT 求解器使用布尔输入。如下表所示：
| 一个 | 乙 | c | d | 电子| | f | 2 | 克 | 3 | h | | 我 | j | ķ | l | 米 |
你可以写a+b+c+f+g+i+j+k = 2和c+d+e+g+h+k+l+m= 3。
问问题
277 次
1 回答
0
如果a+b+c+f+g+i+j+k = 2您的意思是周围的单元格恰好包含两个地雷，那么您的字母确实是布尔变量，并且该约束称为基数约束。
Sat4j 开箱即用地支持这一点。
您可能会在这里找到一些提示： https ://sat4j.gitbooks.io/case-studies/content/
于 2018-03-17T08:19:47.893 回答