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

发布时间：2020-12-16 18:04:11 所属栏目：安全来源：网络整理

导读：我正在尝试寻找解决问题的实用方法(例如在工程方面的努力),其中我有一堆未知值： val a: Int32 = ???val c: Int32 = ???val d: Bool = ??? 和表达式二进制树(在内存中),它最终返回一个布尔值,例如 ((a 4) || (b == (c+2))) (a b) ((2*d)) || e 我所拥有的布

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

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

和表达式二进制树(在内存中),它最终返回一个布尔值,例如

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

我所拥有的布尔运算符是和/或不是和32位整数有比较的东西,以及加法,乘法,除法(注意：这些必须尊重32位溢出！)以及一些按位的东西(移位,按位&,| ^).但是,我不一定需要支持所有这些操作[参见：LOL_NO_IDEA]

我想得到三个答案中的一个：

> ES_POSSIBLE [我不需要知道如何,只是被告知存在一个
它可能是]
>不可能[无论我的变量是什么值
坚持,这个方程永远不会是真的]
> 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”或“是的,你的想法是正确的.享受！”

解决方法

您可能需要查看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/).

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!