最坏情况下X3SAT最大海明距离问题最小上界  

Worst Case Upper Bound for the Maximum Hamming Distance X3SAT Problem

作　　者：傅琳璐[1] 周俊萍[1] 殷明浩[1] 

机构地区：[1]东北师范大学计算机科学与信息技术学院,长春130117

出　　处：《计算机科学与探索》2012年第7期664-671,共8页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金Nos.61070084;60803102;中央高校基本科研业务费专项资金No.11QNJJ006;浙江师范大学计算机软件与理论省级重中之重学科开放基金No.ZSDZZZZXK37~~

摘　　要：X3SAT最大海明距离问题是指对于一个X3SAT问题实例,寻找该问题的任意两组可满足赋值之间的最大海明距离。提出了一个基于DPLL的精确算法HMX来求解X3SAT最大海明距离问题,根据公式中某个变量在两组真值赋值中的不同取值进行分支。给出了多种化简规则,这些规则很好地提高了算法的时间效率。证明了该算法可以将X3SAT最大海明距离问题的最小上界由目前最好的O(1.7107n)缩小到O(1.6760n),其中n为公式中变量的数目。The maximum Hamming distance X-3-satisfiability （X3SAT） problem looks for the maximum Hamming distance between any two x-models of the formula F in 3-conjunctive normal form （3-CNF）. This paper presents an exact algorithm HMX based on Davis-Putnam-Logemann-Loveland （DPLL） for the maximum Hamming distance X3 SAT problem. The algorithm branches on some variable according to its different values in two truth assignments of the formula. Before the branching some reduction rules are used to simplify the formula. The reduction rules increase the efficiency of the algorithm. The worst case upper bound for the problem is O（1.676 0^n）, which improves the previous result O（1.710 7^n）, where n is the number of the variables in the formula.

关 键 词：海明距离 可满足性(SAT) X3SAT DPLL 最坏情况 复杂性分析 上界 

分 类 号：TP301.5[自动化与计算机技术—计算机系统结构]