问题标签 [sat4j]

我在 .dimacs/.cnf 文件中有一个公式，如下所示：

是否可以在 SAT4j 中仅提取那些包含变量 2、3 和 4 的子句？然后，我只需要检查这组新子句的一致性，即：

我尝试使用 Assumptions，我尝试使用 Constraints，但我仍然找不到这样做的方法。

谢谢你的任何建议。

编辑

我认为有一种类似的方法solver.addClause(clause)，但反过来solver.getClause(clause)......虽然，我正在为求解器提供 .cnf 文件中的子句。

编辑 2

首先，假设与子句具有相同的语法，

但变量conjunctions在假设和disjunctions子句中。这是一个区别。正确的？我的测试示例是这样说的。（我只需要获得额外的批准）。

其次，我使用选择器变量的问题是：

一个简单的公式a V b有三个模型：

当我添加一个选择器变量时，例如 ，s并且它的假设是-s，那么我有相同数量的模型，即 3 个模型：

当假设为true时，即 ，s那么我有 4 个模型，而不是我想要的 0：

当然是什么时候s = T，那么(s V a V b) = (T V a V b) = T，但这是对子句的一种删除方式(a V b)吗？我需要的是模型的数量，真实的模型！有没有办法在以某种方式“删除”我们希望通过假设排除的这些变量（即a和）时找到确切的模型？b

对于这种情况，这是我当前在 Scala 中的代码：

感谢您的任何帮助。

我需要从用 Scala 编写的应用程序中调用通用 SAT 求解器。我正在研究 SAT4J，因为它可以很容易地作为 jar 文件导入，但是我发现它很难实际使用。有没有办法可以触发 SAT4j jar 文件来从我的 Scala 代码中计算我的 SAT 问题？

如果 SAT4J 不是正确的方法，是否有任何 SAT 库我可以直接使用而不是启动外部 SAT 求解器？

我是 sat4j 库的新手。我如何定义含义，例如(A1 v A2 v A3) => (A1 ∧ A4)使用 sat4j 并找到所有变量的布尔值？

我找到了 sat4j 的单元测试，而不是我在下面的清单中尝试过的东西。问题是hasASolution()返回 true 但solution变量为空。

我有伪布尔问题，我需要用 sat4j 解决它。

有人能帮我吗？

这是我的问题：

• 我有一个名为：a,b,c,d,e,f 的变量列表

• 我有一个由以下表示的值列表：#1、#2、#3 .....

• h(a,#1) 表示将 #1 分配给 a

我有一些示例约束：

如此多的约束，例如上面的示例。最后，我想要一个将哪个值分配给哪个值的结果。

我怎样才能用 sat4J 解决它？我应该如何表示约束？

我使用 Sat4J 编写了一个 java 程序，它工作正常。现在我想将它导出为 jar 文件，但是当我执行它时，它总是说“发生 JNI 错误，请检查您的安装并重试线程“main”中的异常 java.lang.NoClassDefFoundError: org/sat4j /specs/超时异常”

我对一个以上的包裹没有太多经验。所以我的结构是我有一个包含 4 个我编写的类的包和一个包含 3 个 Sat4J 类的包。我什至不知道是否由于 sat4J 或不同的软件包而发生错误。

有谁知道我能做什么？谢谢。

我正在尝试使用 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。

我想知道 Java SAT4j SAT 求解器 API 如何解决它的伪布尔问题。我浏览过 javadoc，但我对 SAT 问题还是很陌生。

从发布文档（https://www.researchgate.net/publication/220163278_The_Sat4j_library_release_22）中，我认为自定义的伪布尔求解器用于所有事情，而不是反之亦然（伪布尔约束转换为 SAT CNF）。

谁有具体的知识？

在 SAT4J 文档中的代码示例中，对同一个 SAT 问题多次调用求解器总是产生相同的解决方案，即使存在多个可能的解决方案 - 也就是说，结果是确定性的。

我正在寻找一种在多次运行中获得不同解决方案的方法，即非确定性/随机结果。对于每个可能的解决方案，选择该解决方案的概率应该是非零的。理想情况下，应该以相同的概率选择每个解决方案，但这不是严格的要求。

我知道（确定性地）迭代所有解决方案并随机选择一个解决方案的可能性，但在我的情况下这不是一个可行的解决方案，因为有太多的解决方案要开始，并且计算它们都需要很长时间。