【发布时间】：2018-03-16 21:27:29
【问题描述】：
我正在尝试使用 SAT 求解器 (sat4j) 实现扫雷求解器，并且我对它们的工作原理有一个简单的了解。但我不知道的一件事是如何为地雷表示x+y+Z+....=2，因为 SAT 求解器使用布尔输入。如下表所示：
你可以写a+b+c+f+g+i+j+k = 2和c+d+e+g+h+k+l+m= 3。
【问题讨论】：
【发布时间】：2018-03-16 21:27:29
【问题描述】：
如果a+b+c+f+g+i+j+k = 2 是指周围的单元格恰好包含两个地雷，那么您的字母确实是布尔变量，并且该约束称为基数约束。
Sat4j 开箱即用地支持这一点。
您可能会在这里找到一些提示： https://sat4j.gitbooks.io/case-studies/content/
【讨论】：
-
虽然提供的链接没有我要找的东西，但在 SAT4J API 中搜索基数约束给了我正在寻找的方法。谢谢。