|||
姜咏江
逻辑变量的可满足性问题SAT的破解,用子句消去法求解需要解决五个层面的问题。
第一,k阶子句块什么情况下无解?
k阶子句块有2k个不同的子句,则一定无解。例如,3个变量的子句块如果有8个不同的子句,那么合取范式CNF=1一定无解。改变一下判断方法:一个变量在k阶子句块中有2k-1个0和1,那么CNF=1一定无解。
第二,什么情况下变量在子句块中有唯一解?
在k阶子句块中变量只有2k-1个0或1(不同时有)。例如,三个变量的子句块中某变量有4个0,那么这个变量必须取值0。
第三,不同子句块中的同一个变量什么情况下无解?
这就是变量在不同子句块中都有唯一值,但出现了矛盾。即一个值是0,同时在另一个子句块中必须是1,这时合取范式CNF=1无解。
第四,变量的值不是0就是1,可以选择哪个?
变量在子句块中虽然可以取值0或1,但由于子句块间的关联关系,变量取值要受到制约。子句消去过程中不产生矛盾的变量值叫变量可选解。可选解有一个的变量就是关联变量的唯一解。有两个可选解的变量取值,放到最后每个变量都有两个可选解的情况处理。
第五,每个变量都有两个可选解,如何选择变量值?
这种情况下合取范式CNF=1一定有解,但选择值时要避免出现矛盾。因为当前面的变量已经取定0或1的时侯,后面的变量要选择0或1,就要满足前面变量取值的交叉关系,不能出现矛盾选择(有定理保证存在不矛盾取值)。
子句消去法的基本思想是:先将必然选择值的变量确定后,消去相关子句,然后处理可以任意取值的变量,但要避免选择的矛盾。
如果以上五个层面的问题都在消去子句的过程中处理好了,那么任何合取范式的求解都不在话下。
SAT问题最复杂的情况是每个变量都有两个可选解。这时必须将它们的可选解值列表,当要每次选择变量值时,查表依据前面选定值来确定这个变量的值。
由于SAT的二进制数表示的子句总数不超过2Cn1+22Cn2+23 Cn3+...+2(k-1) Cnk-1+2k Cnk,k是常数,这就是一个k次多项式,子句消去法以子句为处理的基本单位,因而子句消去法算法的时间复杂度不会超过O(nk+1)。
k是小于n的常量。上面这个多项式与2n相比,只有当n大到一定程度,才会体现出多项式算法的“快速”性。如果k很大,仍然会感到“很慢”,但由于合取范式CNF有很多特别情况,研究这些特别情况,可以得到比DPLL算法快得多的算法。
2017-2-6
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-12-22 01:19
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社