scala - 检查表达式树的可满足性

Question

我正在尝试寻找解决问题的实用方法(例如在工程方面)，其中我有一堆未知值:

val a: Int32 = ???
val c: Int32 = ???
val d: Bool = ???

和一个表达式二叉树(在内存中)，最终返回一个 bool 值，例如

((a > 4) || (b == (c+2))) && (a < b) && ((2*d)) || e

我拥有的 bool 运算符是 and or xor not并且 32 位整数具有比较之类的东西，以及加法、乘法、除法(注意:这些必须尊重 32 位溢出!)以及一些按位的东西(移位、按位 &、| ^ )。但是，我不一定需要支持所有这些操作 [参见:LOL_NO_IDEA]

我想得到三个答案之一:

ES_POSSIBLE [我不需要知道如何，只是被告知存在一个
可能的方式]

UNPOSSIBLE [无论我的变量值如何
持有，这个等式永远不会是真的]

LOL_NO_IDEA [这是
可以接受，如果问题太复杂或太耗时]

我要解决的问题都不是太大或太复杂，术语太多(最多是数百个)。并且拥有大量的 LOL_NO_IDEA 很好。然而，我正在解决数以百万计的此类问题，因此持续的成本会令人痛苦(例如，转换为文本格式，并调用外部求解器)

由于我是从 scala 执行此操作的，因此使用 SAT4J 看起来非常吸引人。虽然，文档很糟糕(尤其是像我这样的人，他只研究了这个 SAT 世界几天)

但我目前的想法是首先将所有 Int32 转换为 32 个 bool 值。这样，我可以通过将其作为嵌套 bool 表达式来表达(a < b)之类的关系(比较 msb，如果它们是 eq，则为下一个，等等)

然后当我有一个 bool 变量和 bool 表达式的大表达式树时——然后遍历它，同时逐步建立一个:
http://en.wikipedia.org/wiki/Conjunctive_normal_form

然后将其输入SAT4J。

然而，所有这些看起来都非常具有挑战性——甚至构建 CNF 似乎也非常低效(以天真的方式进行，我会实现它)并且容易出错。更不用说尝试将所有整数数学编码为 bool 表达式。而且我还没有找到为像我这样的人设计的好资源

我会很感激任何反馈，
即使它就像“大声笑，你是个白痴——看看X”或“是的，你的想法是正确的。享受吧!”

Answer 1

您可能想看看 Z3 (http://z3.codeplex.com/)，或其他一些可满足性模理论 (SMT) 求解器。据我所知，您所说的问题涉及线性整数算术或可能的位向量。我想我更喜欢有一个对这些理论有一定了解的求解器，而不是只用 bool 值来编码问题。

Z3 具有 Java 绑定(bind)(参见 http://research.microsoft.com/en-us/um/people/leonardo/blog/2012/12/10/z3-for-java.html)。不过，我自己并没有使用过它们，并且不确定有多少开销。

使用 SAT 求解器时，您通常不必自己将问题放入 CNF。求解器应预处理您的公式(通常通过 Tseitin 变换 http://en.wikipedia.org/wiki/Tseitin-Transformation )。

您可以研究的另一个选项是约束满足。我知道 Choco (http://www.emn.fr/z-info/choco-solver/)。