如何在java中使用sat4j为布尔公式的变量赋值？

Question

对于sat4j求解器和布尔可满足问题的研究，我是完全陌生的，我想要编制一个程序来解决布尔公式中的整数变量。

x1 < x2 + x3用户输入该公式，我的程序满足这个公式(返回真)，如x1 =5，x2 = 3，x3 = 4。因此，公式返回true，用户获得满足formula.Is的整数值，因为我使用java在eclipse中使其在sat4j中成为可能。

Answer 1

不确定SAT4J是否解决了…您应该寻找支持线性算法的SMT求解器(您的情况似乎只有不同的逻辑才能做到)。您可以检查: Z3 (微软的SMT解决程序)、CVC4和Yices。更广泛的列表在这里：theories

希望这能帮上忙。