我是 sat4j 求解器的新手..

它说应该给出一些cnf文件作为输入

是否有任何可能的方法将规则作为输入并获取它是否可以满足？

我的规则是这样的：

有人可以帮助我如何使用 sat4j 求解器解决这个问题吗？

我正在尝试使用SAT4J解决以下问题。我的问题是如何使用他们的 API 向 SAT4J 指定问题。

这是问题所在：

这样：

我正在尝试使用 SAT 求解器 SAT4J 解决部分加权最大可满足性问题。

我的 .wcnf 文件很大，它包含大约一百万个约束。

当我运行求解器时，我得到以下作为输出的一部分(OutOfMemoryError : Java heap space)：

也就是说，堆空间不足错误。如何增加堆空间的大小以及将其增加到什么合适的值？

这就是我在约束文件 constraints.wcnf 上调用 sat4j 求解器的方式：

/usr/bin/java -jar sat4j-maxsat.jar constraints.wcnf

谢谢

怎么了：

我执行以下命令。

没有窗口打开，我得到一个控制台输出，与没有 -remote 标志的情况相同，它开始：

预期：

来自 readme.txt：

使用动态配置运行 sat4j：

这些说明应该会打开一个名为 Remote Control 的 java 窗口。我们假设 1.5 版本的 java 命令在您的路径中。如果不是，那么您应该指定 java 命令的完整路径或更新您的 PATH 环境变量，如 Java 2 SDK 的安装说明中所述。

其他详情

我尝试了该库的多个版本，最高为 2.3.4。

我的系统是带有 Gnome 2 的 Debian 7。

我的默认 Java 安装是 OpenJDK 1.7.0_65。

我的辅助 Java 安装是 Oracle Java 1.8.0_45（同样的问题）。

安装了 Gnuplot 4.6。

我的第一台机器有一个 32 位双核 CPU 和 2GB 内存。

我的第二台机器有一个 64 位四核 CPU 和 8GB RAM，软件几乎相同。

问题

有人用过SAT4J的遥控功能吗？我的方法有什么问题？

更新

在另一台机器（64 位 Debian 7）上，该窗口打开。开始后创建 dat 文件，但绘图未开始。

更新 2

我从 gnuplot 终端手动运行生成的instance.dimacs-gnuplot.gnuplot文件，并收到了unknown or ambiguous terminal type该x11类型的消息。我安装了该gnuplot-x11软件包，现在它可以在工作场所的机器上运行：我可以看到图表（哇！）。不幸的是，在我的家用机器上，远程控制窗口仍然没有打开。

我的 Java 程序从其数据生成一个大型 CNF 实例。该实例主要包含（在大多数情况下>95%）排他的 2 子句：(!av !b)。目前我使用 Sat4j 的默认求解器。当我启用程序中的所有条件时，求解器将无限期运行。我尝试过一些经验来优化启发式和配置，但没有成功。解决此类情况的适当启发式集是什么？

（一个例子。）

我对 sat4j 求解器和研究布尔可满足问题是全新的；我被卡住了。我想制作一个程序来解决布尔公式中的整数变量，例如；

x1 < x2 + x3 用户输入该公式，我的程序满足该公式（返回真），如 x1 = 5 ，x2 = 3，x3 = 4。所以公式返回真，用户得到满足公式的整数值。是可以在 sat4j 中实现它，因为我使用 java 在 eclipse 中工作。

我正在尝试为我的学校项目构建 N*N 皇后安置问题解决器。我制作了一个程序，即生成 CNF 语句。我试图将其地址作为“SAT4J 嵌入求解器”第 7 页 3.1的参数，但是它一直抛出 ParseFormatException。我还尝试使用我在 stackoverflow 上找到的这个文本文件：

也没有运气。我唯一编辑的是异常的捕获块，所以我可以看到它是哪一个。我正在尝试通过 IntelliJ Idea Community 版中的 Alt+Shift+F10 配置菜单为其提供参数。

有人可以帮我/指导我吗？这是我第一次使用其他人的代码 + 没有任何可用的教程。

也许，你可以建议我其他方式。我只需要 SAT 求解器来解决这个问题并给我输出，所以我可以用它来制作棋盘的图形表示:)

截至目前的课程代码。

据我了解，增量 SAT 求解有助于评估彼此非常接近的不同模型。

我想用它来评估模型，如果我稍后更改它，使用以前的解决方案再次重新评估它以获得更快的结果。然而，在研究了各种 SAT 求解器（Sat4J、Minisat、mathsat5）之后，似乎它们只能在一次运行中呈现所有模型时才能增量求解。

我对SAT解决很陌生，所以我可能会忽略一些东西。有没有办法保存解决实例供以后使用？关闭实例会丢失所有学习内容吗？

我刚刚开始使用 Sat4j 库。你能指导我如何计算解析和简化给定 CNF 输入所需的时间吗？

我用过

我希望计算读者解析和 isSatisfiable 所花费的时间。如果可能，请指导我在图像中查找每个处理过的 cnf 文件 的信息 我希望使用 sat4j lib 收集的详细信息的屏幕截图 提前感谢您的时间。

我之前没有用过SAT求解器，所以我开始学习如何使用SAT4J。大多数情况下，我使用它的 API，但有时我发现很难理解某些参数（在类或方法中）的含义或它们的格式/类型是可以接受的。例如：

我的问题是是否有一些使用示例，可​​以帮助我更多地理解 SAT4j 中实现的功能？

先感谢您！