为什么 MiniSat、MiniSat with Unsat Core、Lingeling、Glucose 等求解器选项没有出现在我的 Alloy*/Alloy 工具中？答案

【问题标题】：Why do solver options like MiniSat, MiniSat with Unsat Core, Lingeling, Glucose do not appear in my Alloy*/Alloy tool?为什么 MiniSat、MiniSat with Unsat Core、Lingeling、Glucose 等求解器选项没有出现在我的 Alloy*/Alloy 工具中？
【发布时间】：2015-10-05 20:42:48
【问题描述】：

在我下载的工具中： http://alloy.mit.edu/alloy/hola/

出现的求解器的唯一选项是 SAT4J 和 PLingeling。为什么其他选项也没有出现？我正在使用 Windows 并通过双击文件 hola-0.2.jar 来执行该工具...

从以下位置下载的合金工具也会出现同样的错误： http://alloy.mit.edu/alloy/download.html

但是，当我在 Windows 7 中运行它时，会出现诸如 miniSAT、带有 Unsat Core 的 miniSAT、ZChaff 之类的求解器选项！可用的求解器选项取决于操作系统？

【问题讨论】：

标签： options solver alloy

【解决方案1】：

像 minisat 这样的求解器不是基于 java 的。因此，Alloy Analyzer 为每个常用操作系统提供了这些求解器的本机版本。如果您使用存档器打开 .jar，您将能够看到四个文件夹：x86-windows、x86-mac、x86-linux 和 x86-freebsd，每个文件夹都包含与这些求解器相关的特定于操作系统的可执行文件。

在您的问题中，您说在 Windows 上使用这些求解器时遇到问题，但说在 Windows 7 上一切正常。因此，我可以假设 Windows 是指 Windows 操作系统的最新版本，即 Windows 10 吗？

我不熟悉它，但可能是 x86_windows 文件夹中的那些 .dll 根本无法在 Windows 10 上按预期工作。

【讨论】：

嗨 Loic，谢谢你的回答。我有两台在 Windows 7 上运行的机器——其中一台出现了 miniSat 等求解器。此外，我还有另一台机器在 Windows 8 上运行，只有求解器 SAT4J 作为选项出现（在另一台 Windows 7 机器中呈现相同的行为）。

【解决方案2】：

您使用的是哪个 Java 版本（32 位或 64 位）？

alloy download page 包含一个 jar 文件，其中包含用于 x86_windows 的本机库/解算器，即在 Java 32 位中工作但在 Java 64 位中不工作的库。考虑到 Alloy 使用 JNI 和这些库来运行求解器，您必须使用适当的 Java 版本才能使用求解器。

Alloy jar 文件包括适用于 Windows、Mac 和 FreeBSD 的 32 位本机库，以及适用于 Linux 的 32 位和 64 位库。

【讨论】：