java - 如何在java中使用sat4j将整数值分配给 boolean 公式的变量？-6ren

java - 如何在java中使用sat4j将整数值分配给 boolean 公式的变量？

转载作者：行者123 更新时间：2023-11-30 03:10:16

24

4

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

x1 < x2 + x3 用户输入该公式，我的程序满足该公式(返回 true)，例如 x1 = 5 、 x2 = 3、x3 = 4 。因此，公式返回 true 并且用户获得满足以下条件的整数值:公式。是否可以在 sat4j 中制作它，因为我在 eclipse 中使用 java 工作。

最佳答案

不确定 SAT4J 是否可以进行 SMT 求解...您应该寻找支持线性算术的 SMT 求解器(您的情况似乎只有差分逻辑也可以)。您可以检查:Z3(Microsoft 的 SMT 求解器)、CVC4 和 Yices。更详细的列表在这里:https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

希望这有帮助...

关于java - 如何在java中使用sat4j将整数值分配给 boolean 公式的变量？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/33760998/

24

4

0

文章推荐： java - 如何在 Android 中使用 runnable 循环

文章推荐： javascript - 如何在 Google V8 引擎中创建一个 utf8 字符串

文章推荐： java - Getter 总是返回 Null 值

algorithm - C-SAT 和 SAT 的区别？
这两个 NP 完全问题之间到底有什么区别？在我看来，他们都在询问是否可以满足 bool 公式(即输出 1)，但一个是在电路的上下文中，另一个只是一个公式。但是，不能从 bool 电路中写出 bool
algorithm - 从 SAT 到 3-SAT 的转换器
有谁知道一个好的程序可以将每个子句具有任意数量变量的 CNF 文件转换为每个子句恰好有 3 个变量的 CNF 文件 (3-CNF)？我在计算机科学书籍中看到过这种算法，但无法在任何地方找到实现，如果其
algorithm - Max 2 Sat 究竟如何减少到 3 Sat？
我一直在阅读 this文章尝试并解释了 max 2 sat 问题本质上是一个 3-sat 问题并且是 NP-hard。然而，如果你看到这篇文章，我无法理解为什么，满足ci后，10个子句中有7个是满意
z3 - (check-sat) vs (check-sat-using smt)
看完strategies guide Z3 和 this answer利奥，我预计(check-sat)和 (check-sat-using smt)是等价的。然而，当针对我们的测试套件(230 个
logic - SAT 的特殊情况和相应的#SAT 复杂度最高为 O(n^2) 并且具有用于生成实例的有效算法？
我有兴趣了解已知为多项式(或更现实地说，O(N^2))的 bool 可满足性问题的特殊情况。这些案例还应该有有效的算法来实际生成所有令人满意的实例，其中高效我的意思是需要 O(N #SAT) 来生成所
z3 - 仅当 check-sat 返回 "sat"时才动态调用 get-value
SMT2 标准规定，调用 get-value 仅在调用 check-sat 之后才合法，并且仅当 check-sat 返回“sat”或“unknown”时才合法。下面是一个 unsat 问题的简单示
algorithm - 将 Not All Equal 2-Sat 问题转换为等效的 2-SAT 问题
我正在翻阅以前的试卷，并且遇到了这个让我感到困惑的问题。问题: Convert the Not-All-Equal 2-SAT problem given by the clauses {x1, x
go - x := [. ..] 字符串 {"Sat", "Sun"} vs x := []string {"Sat", "Sun"}
在 go 语言中 spec他们在其中一个示例中使用了三个点: days := [...]string{"Sat", "Sun"} // len(days) == 2 如果省略这三个点有什么不同吗？
algorithm - 2-CNF SAT 如何在 P 中，而 3-CNF SAT 在 NPC 中？
我真的很困惑为什么2-CNF SAT在P，而3-CNF SAT在NPC。我读过 CLRS，我了解他们如何证明 3-CNF SAT 在 NPC 中。我不能使用从 SAT 到 2-CNF-SAT 的相同还
sat - MiniSat 中非决策变量的语义是什么？
当使用 MiniSat 作为 C++ 库时，每个新变量都可以创建为决策变量或非决策变量。我对此的粗略理解是，当求解器在分支期间决定接下来使用哪个变量时，不考虑非决策变量。然而，在我的项目中，当非决策
z3 - 为大问题获取 'sat'
我从模板生成问题，由于问题的性质，我不得不依赖量词。现在，求解器只能找到非常简单(可满足)问题的实例。在许多情况下，寻找“unsat”是可行的。查找“sat”很少奏效。问题在于，即使是像定义两个不相
Prolog SAT 求解器
我正在尝试构建一个简单的 Prolog SAT 求解器。我的想法是用户应该使用 Prolog 列表输入要在 CNF(联合范式)中求解的 bool 公式，例如(A 或 B)和(B 或 C)应显示为 sa
python - SAT 最小翻译向量不正确
SAT 的最小翻译向量是否在所有情况下都始终正确和精确？我通过迭代所有可能的轴并检查每个轴上的重叠来计算它，然后继续跟踪哪个轴具有最短的重叠并将其用作穿透向量。如您所见，最小平移向量的某些计算并不总
algorithm - SAT 求解器确定多元函数的特征？
Boolean Satisfiabiity problem是检查 bool 表达式的可满足性的概括。现在 bool 表达式是由多项式的非负性算法生成的。例如，多项式可以是和有一些间隔，例如其中
algorithm - SAT/CNF优化
问题我正在研究 SAT 优化问题的一个特殊子集。对于那些不熟悉 SAT 和相关主题的人，这里是 related Wikipedia article . TRUE=(a OR b OR c OR d)
F# Or-Tools Sat 求解器
我正在试验 F#，并希望在我使用 Or-Tools 的地方进行一些约束编程。我以前将该包与 Python 一起使用，但我无法让它与 F# 一起使用。我遵循 C# 示例:https://develop
python - CP-SAT 天花板
在调度问题中。我想按工作天数分配假期。现在我有一个使用多个 bool 标志的有效解决方案，但它的扩展性不是很好。 from ortools.sat.python import cp_model fro
satisfiability - 可以使用 SAT 求解器找到所有解吗？
我写了一个我认为是 quite interesting question 的答案，但不幸的是，在我发布之前，该问题已被作者删除。我在这里重新发布问题的摘要和我的答案，以防其他人有用。假设我有一个 S
logic - 求解命题逻辑规则集中的特定组合(SAT Solver)
在汽车行业，当您购买汽车时，您有数千种不同的组件可供选择。并非每个组件都是可组合的，因此对于每辆汽车，都存在许多用命题逻辑表达的规则。就我而言，每辆车都有 2000 到 4000 条规则。它们看起来
无法编译和运行 minisat+ sat 求解器
我在大学系使用一台 Cent0S 机器。请注意，我没有权限使用我作为 root 使用的系统。我下载了 minisat+zip file 我解压了zip。根据我运行的安装文件 make rx 但我有以下

首页

博学

6Ren·AI

商城

java - 如何在java中使用sat4j将整数值分配给 boolean 公式的变量？