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

Question

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

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

Answer 1

不确定SAT4J是否进行SMT解决。。。您应该寻找支持线性算术的SMT求解器（您的案例似乎只有差分逻辑也可以）。您可以检查：Z3（来自Microsoft的SMT解算器）、CVC4和Yices。更广泛的列表如下：https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

希望这能帮助。。。