检查表达式树的可满足性

Question

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

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 <b)这样的关系(比较msb,如果它们是eq,那么下一个等等)

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

然后将其喂入SAT4J.

然而,所有这些看起来都非常具有挑战性 - 甚至构建CNF似乎效率很低(以天真的方式做,我实现它)并且容易出错.更不用说尝试将所有整数数学编码为布尔表达式.而且我无法为像我这样的人找到好的资源,一个想要使用SAT解决问题的工程师主要是一个黑盒子

我很感激任何反馈,即使它像"哈哈,你的白痴 - 看看X"或"是的,你的想法是正确的.享受!"

Answer 1

您可能需要查看Z3(http://z3.codeplex.com/)或其他一些可满足性模数理论(SMT)求解器.你所说的问题涉及线性整数算术或可能是bitvectors,据我所知.我想我更愿意让一个解决者对这些理论有所了解,而不是只用布尔人编码问题.

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/).