问合金-找不到未满足的核心

EN

你只看到SAT4J？检查一下:你点击了Options菜单，然后点击了Solver: SAT4J这行，对吧？

当你这样做的时候，你应该得到一个带有SAT求解器列表的子菜单；在我的系统上，它看起来像这样：

​

​

我希望这能帮到你。如果没有，我希望下一件事是什么构建关于合金对话框显示。(作为比较:刚刚给出的屏幕截图是由2014-05-16版本生成的。)

Postscript

阿。正确的。您的经验表明，the documentation中的这句话是什么意思

缺省情况下，选择纯

求解器"SAT4J“，因为它可以在每个平台和操作系统上运行。如果需要更快的性能，可以尝试本地解算器之一，如MiniSat或ZChaff。

我从(现在)推断出，SAT4J以外的求解器并不都是纯Java的(或者它们中的任何一个)，而是需要一个本机接口(即用其他语言编写的代码的接口)。如果JNI不能在您的平台上工作，正如您的警告消息所指出的，SAT4J可能是唯一可用的求解器。

也许开发团队中的某个人可以发表评论。

因此，如果你不能切换到Unsat作为一种方法来找出为什么你的模型没有实例，你就会回到其他方法上。

一种方法是显而易见的(尽管有点乏味)：通过模型中的约束集进行二进制搜索。

如果你明白我的意思，但又想不出更好的方法，那么祝你好运。

如果你知道我的意思，并能想到更好的方法，请告诉我们其他人是什么。

如果你不知道我的意思，我脑海中的方法类似于一种广泛使用的技术，当你不知道语法错误在哪里的时候，它可以用来查找程序中的语法错误。(一个模糊的记忆告诉我，我可能是从Jon Bentley的Programming Pearls中学到这一点的。也许吧。)这里有一种方法可以做到。

1. 在模型的当前状态下对其进行备份。稍后，当您开始怀疑这个或那个小细节是否已更改时，您将需要它。
2. 将您的所有命名事实更改为命名谓词。(如果证明有必要，还要将所有签名事实，甚至其他约束，更改为命名谓词。我只在别无选择的情况下才这样做，因为它需要重写比我希望的更多的模型。)
3. 生成一个新的谓词ANDing所有的命名谓词。在接下来的内容中，我将把它称为AllTogetherNow。它的形式类似于

pred AllTogetherNow { P1 P2 P3 ...Pn }

此时，您的模型应该由签名(带或不带签名事实)和命名谓词组成，而不是事实。

1. 检查以确保在AllTogetherNow不为true时可以实例化模型。

如果它不能被实例化，并且您仍然有签名事实，那么返回到步骤2，并将它们中的一些或全部提取出来。修订AllTogetherNow以包含新分解的约束。

如果它不能被实例化，并且您没有任何签名事实，那么返回到步骤2，并从签名的基数约束中提取出隐含的约束。修改AllTogetherNow以包含新分解的constraints.

• Check，以查看AllTogetherNow是否可以实例化。

如果它可以实例化，那么您的原始模型和现在的模型之间发生了一些变化。改变的东西是原始model.

• Comment中的错误，也就是当前存在于AllTogetherNow中的一半谓词，它们要么通过cunning选择，要么在random.

• Check中选择，以查看AllTogetherNow是否可以实例化。

如果不能，那么AllTogetherNow中当前存活的谓词的某个子集就包含了一个矛盾。返回到步骤6，注释掉更多谓词。

如果AllTogetherNow现在可以实例化，那么您刚才注释掉的谓词的某个子集就是模型不能像最初编写的那样实例化的原因。继续执行步骤8.

• 取消注释当前在AllTogetherNow中注释掉的一半约束，可以是随机选择的，也可以是巧妙地选择的。返回步骤7.

我的经验是，通过步骤6-8的几个循环通常可以帮助我足够集中注意力，最终我可以看到矛盾之处。我遇到的主要复杂性(YMMV)是(1)一个人的初始草案模型并不局限于单个矛盾，(2)矛盾可能产生于单独无害的谓词的不愉快组合，以及(3)建立矛盾组合的方法可能不止一种(谓词、A、B、C和D各自都很好；A与B或C结合在一起是致命的……)。

可能出现的一个心理困难是，矛盾不是出现在模型的“有趣”部分，而是在一个人试图为有趣的问题设置舞台时。除了告诉自己，任何意想不到的矛盾都会自然而然地变得有趣，值得花费时间在上面，我不知道有什么解决办法。有时我能够说服自己。