检查表达式树的可满足性答案

【问题标题】：Checking satisfiability of expression tree检查表达式树的可满足性
【发布时间】：2013-04-07 17:14:51
【问题描述】：

我正在尝试寻找一种实用的方法（例如在工程方面）来解决一个问题，其中我有一堆未知值：

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

和一个表达式二叉树（在内存中），最终返回一个布尔值，例如

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

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

我想得到三个答案之一：

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

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

但我目前的想法是首先将所有 Int32 转换为 32 个布尔值。这样，我可以通过将其作为嵌套布尔表达式来表达（a

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

然后将其输入 SAT4J。

但是，所有这些看起来都非常具有挑战性——甚至构建 CNF 似乎也非常低效（以天真的方式进行，我会实施它）并且容易出错。更不用说尝试将所有整数数学编码为布尔表达式。而且我还没有找到为像我这样的工程师设计的好的资源，这个工程师有一个问题，想将 SAT 解决方案作为一个黑匣子来使用

如果有任何反馈，我将不胜感激，即使它就像“大声笑，你是个白痴——看看X”或“是的，你的想法是正确的。享受吧！”

【问题讨论】：

【解决方案1】：

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

Z3 具有 Java 绑定（请参阅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/)。

【讨论】：

【解决方案2】：

由于您是 scala 程序员，您可能想直接使用 scala 库，例如 Scarab http://kix.istc.kobe-u.ac.jp/~soh/scarab/ 此类工具为您提供 Scala 中问题的建模，并通过 SAT 求解器解决问题。

【讨论】：

这看起来真的很棒！我要么会使用它，要么至少大量使用它作为参考 =)
你知道使用这样的东西有多高效吗，我所有的整数都是这样的： int('x, INT.MIN, INT.MAX) ？这会导致它爆炸，我应该手动将它爆炸成布尔值吗？还是应该没问题？
好吧，它肯定会爆炸。通常模型检查是使用有限长度的整数来执行的（像 Alloy alloy.mit.edu 这样的工具在默认情况下仅使用 4 位整数……）如果您确实需要操作完整的整数，则应该采用 SMT 方式。