我对 sat4j 求解器和研究布尔可满足问题是全新的；我被卡住了。我想制作一个程序来解决布尔公式中的整数变量，例如；
x1 < x2 + x3 用户输入该公式，我的程序满足该公式（返回真），如 x1 = 5 ，x2 = 3，x3 = 4。所以公式返回真，用户得到满足公式的整数值。是可以在 sat4j 中实现它，因为我使用 java 在 eclipse 中工作。
问问题
302 次
1 回答
2
不确定 SAT4J 是否进行 SMT 求解...您应该寻找支持线性算术的 SMT 求解器（您的情况似乎只有差分逻辑也可以）。您可以查看：Z3（Microsoft 的 SMT 求解器）、CVC4 和 Yices。更广泛的列表在这里：https ://en.wikipedia.org/wiki/Satisfiability_modulo_theories
希望这可以帮助...
于 2015-11-18T09:47:02.613 回答