d-正则(k,s)-SAT问题的NP完全性

研究具有正则结构的SAT问题是否是NP完全问题,具有重要的理论价值.(k,s)-CNF公式类和正则(k,s)-CNF公式类已被证明存在一个临界函数f(k),使得当s≤f(k)时,所有实例都可满足;当s≥f(k)+1时,对应的SAT问题是NP完全问题.研究具有更强正则约束的d-正则(k,s)-SAT问题,其要求实例中每个变元的正负出现次数之差不超过给定的自然数d.通过设计一种多项式时间的归约方法,证明d-正则(k,s)-SAT问题存在一个临界函数f(k,d),使得当s≤f(k,d)时,所有实例都可满足;当s≥f(k,d)+1时,d-正则(k,s)-SAT问题是NP完全问题.这种多项式时间的归约变换方法通过添加新的变元和新的子句,可以更改公式的子句约束密度,并约束每个变元正负出现次数的差值.这进一步说明,只用子句约束密度不足以刻画CNF公式结构的特点,对临界函数f(k,d)的研究有助于在更强正则约束条件下构造难解实例.     

一个正则NP-完全问题及其不可近似性

通过一个适当的归约变换,可以将一个CNF (conjunctive normal form)公式变换为另一个具有某种特殊结构或性质的公式,使两者具有相同的可满足性.带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果,可以用于研究公式的可满足性和计算复杂性.极小不可满足公式具有一个临界特征,公式本身不可满足,从原始公式中删去任意一个子句后得到的公式可满足.借助此临界特性,给出了一个从3-CNF公式到正则(3,4)-CNF公式的多项式归约转换.这里,正则(3,4)-CNF公式是指公式中每个子句的长度恰为3,每个变元出现的次数恰为4.因此,正则(3,4)-SAT问题是一个NP-完全问题,并且MAX(3,4)-SAT是不可近似问题.     

基于因子图求解(3,4=)-CNF公式类下可满足问题

合取范式(CNF)公式F是(3,4=)-CNF公式,如果F中每个子句的长度是3,每个变元出现的次数恰好为4次.与(3,4=)-CNF公式所关联的因子图是一类规则的二部图,即每个子句结点的度为3,每个变元结点的度为4,此类规则图被称为(3,4)-双向正则二部图.对于一个(3,4=)-CNF公式F,如果它关联的因子图GF有P7路径因子,则F可满足.     

用于求解正则(3,4)-SAT实例集的修正警示传播算法

利用极小不可满足公式的临界特性,可以将任意的一个3-CNF公式多项式时间归约转换为一个正则(3,4)-CNF公式,从而得到一个保留NP完全性的正则(3,4)-SAT问题。警示传播算法(Warning Propagation,WP)在归约转换后的正则(3,4)-SAT实例集上高概率收敛,但在任意一个实例上都无法判断公式的可满足性,因此算法求解失效。对于一个归约转换后的正则(3,4)-CNF公式,每一变元出现的正负次数之差具有趋于稳定的结构特征,基于该特征,提出基于变元正负出现次数规则的WP算法来求解归约转换后的正则(3,4)-SAT实例。实验结果表明,修正的WP算法对正则公式的可满足性判定有效,从而可以利用公式的正则性特征进一步研究WP算法的收敛性特征条件。     

正则3-SAT问题的相变现象

通过对3-CNF公式加以限制,要求其中每个变元出现的次数相同,引出正则3-SAT问题。进一步,通过对两种子句产生机制形成的(3,s)-CNF公式进行可满足性观察,发现在规模较小的情况下,正则3-CNF公式比非正则3-CNF公式更容易满足。从而推测与非正则3-SAT问题相比,正则3-SAT问题的相变点有偏移现象。最后,从变元自由度的角度对这一现象给出了定性解释。     

极小不可满足公式在多项式归约中的应用

合取范式(CNF)公式F是极小不可满足的,如果F不可满足,并且从F中删去任意一个子句后得到的公式可满足,(r,s)-CNF是限制CNF公式中每个子句恰有r个不同的文字,且每个变元出现的次数不超过s次的公式类,对应的满足性问题(r,s)-SAT指实例公式限制于(r,s)-CNF.对于正整数r≥3,有一个临界函数f(r),使得(r,f(r))-CNF中的公式都是可满足的,而(r,f(r)+1)-SAT却是NP-完全的.函数f是否可计算是一个开问题,除了知道f(3)=3,f(4)=4外,只能估计f(r)的界.描述了极小不可满足公式在CNF公式类之间转换中的作用.为使转换过程中引入较少的新变元,给出了CNF公式到3-CNF公式的一种新的转换方法,对于长度为l(＞3)的子句,仅需引入|l/2|个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法.     

正则(3,4)-CNF公式的社区结构

通过构造适当的极小不可满足公式以实现在多项式时间内将3-CNF公式归约转换为一个正则(3,4)-CNF公式,转换后的公式与原公式具有相同的可满足性,同时公式的结构也发生相应的变化。图的社区结构反映了图的模块特性,文中将CNF公式转化为相应的图,研究公式图的模块特性与公式某些性质之间的关系。将归约前后的两类公式转换为相应的图并研究其模块特性,发现转换后得到的正则(3,4)-CNF公式具有较高的模块度。此外,在使用DPLL(Davis Putnam Logemann Loveland)算法求解CNF公式的过程中,发生冲突时利用冲突驱动子句学习策略,得到一个学习子句并将其添加到原公式中,使得原公式的模块度降低。研究发现:将DPLL算法与冲突驱动子句学习策略结合应用到正则(3,4)-CNF公式时,其学习子句所包含的绝大部分变元位于不同的社区中。     

求解多文字可满足SAT问题的置信传播算法

可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真.多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真.显然,此问题仍然是一个NP难问题.为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法.最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法.     

多文字可满足SAT问题的相变点上界

可满足(SAT)问题是指：是否存在一组布尔变元赋值,使得随机合取范式(CNF)公式中每个子句至少有1个文字为真。多文字可满足SAT问题是指：是否存在一组布尔变元赋值,使得随机CNF公式中每个子句至少有2个文字为真。此问题仍然是一个NP难问题。定义约束密度α为CNF公式子句数与变元数之比,对该问题的相变点上界α^*进行了研究。如果α>α^*,则多文字可满足SAT问题高概率不可满足。通过一阶矩一个简单的推断,可以证明α^*=-ln 2/ln(1-(k+1)/2^k),当k=3时,α^*=1。利用Kirousis等人的局部最大值技术,提升了多文字可满足3-SAT问题的相变点上界α^*=0.7193。最后,选择了大量数据进行实验验证,结果表明,理论结果与实验结果相吻合。     

取定s的严格d-正则随机(3,2s)-SAT问题的可满足临界

3-CNF公式的随机难解实例生成对于揭示3-SAT问题的难解实质和设计满足性测试的有效算法有着重要意义.对于整数k>2和s>0,如果在一个k-CNF公式中每个变量正负出现次数均为s,则称该公式是严格正则（k,2s）-CNF公式.受严格正则（k,2s）-CNF公式的结构特征启发,提出每个变量正负出现次数之差的绝对值均为d的严格d-正则（k,2s）-CNF公式,并使用新提出的SDRRK2S模型生成严格d-正则随机（k,2s）-CNF公式.取定整数5<s<11,模拟实验显示,严格d-正则随机（3,2s）-SAT问题存在SAT-UNSAT相变现象和HARD-EASY相变现象.因此,立足于3-CNF公式的随机难解实例生成,研究了严格d-正则随机（3,2s）-SAT问题在s取定时的可满足临界.通过构造一个特殊随机实验和使用一阶矩方法,得到了严格d-正则随机（3,2s）-SAT问题在s取定时可满足临界值的一个下界.模拟实验结果验证了理论证明所得下界的正确性.     

基于聚类和划分的SAT分治判定

提出了一种将布尔公式划分为子句组来进行布尔可满足性判定的方法.CNF(conjunctive normal form)公式是可满足的当且仅当划分产生的每个子句组都是可满足的,因此,通过判定子句组的可满足性来判定原公式的可满足性,相当于用分治法将复杂问题分解为多个子问题来求解.这种分治判定方法一方面降低了原公式的可满足性判定复杂度;另一方面,由于子句组的判定可以并行,因而判定速度能够得到进一步的提高.对于不能直接产生布尔子句组划分的情形,提出了一种利用聚类技术将CNF公式聚类成多个簇,然后消去簇间的公共变量来产生子句组划分的方法.     

Exact Algorithms for MAX-SAT

The maximum satisfiability problem (MAX-SAT) is stated as follows: Given a boolean formula in CNF, find a truth assignment that satisfies the maximum possible number of its clauses. MAX-SAT is MAX-SNP-complete and received much attention recently. One of the challenges posed by Alber, Gramm and Niedermeier in a recent survey paper asks: Can MAX-SAT be solved in less than 2ⁿ “steps”? Here, n is the number of distinct variables in the formula and a step may take polynomial time of the input. We answered this challenge positively by showing that a popular algorithm based on branch-and-bound is bounded by O(2ⁿ) in time, where n is the maximum number of occurrences of any variable in the input.When the input formula is in 2-CNF, that is, each clause has at most two literals, MAX-SAT becomes MAX-2-SAT and the decision version of MAX-2-SAT is still NP-complete. The best bound of the known algorithms for MAX-2-SAT is O(m2^m/5), where m is the number of clauses. We propose an efficient decision algorithm for MAX-2-SAT whose time complexity is bound by O(n2ⁿ). This result is substantially better than the previously known results. Experimental results also show that our algorithm outperforms any algorithm we know on MAX-2-SAT.     

The Complexity of Pure Literal Elimination

The computational complexity of eliminating pure literals is calibrated for various classes of CNF formulas. The problem is shown to be P-complete in general, NL-complete for 2-CNF, and SL-complete for CNF formulas with at most two occurrences of each variable.     

基于关键文字的求解SAT问题的启发式算法

逻辑公式的可满足问题的求解方法是近几年研究的重点,通过对逻辑公式的关键文字和骨干变元集的研究与分析,使用启发式算法寻找公式的关键文字,在公式化简中引入关键文字规则,给出了一种新的求解SAT问题的启发式算法。     

一类可分离SAT问题的O(1.890n)精确算法

布尔可满足性问题（SAT）是指对于给定的布尔公式,是否存在一个可满足的真值指派.这是第1个被证明的NP完全问题,一般认为不存在多项式时间算法,除非P=NP.学者们大都研究了子句长度不超过k的SAT问题（k-SAT）,从全局搜索到局部搜索,给出了大量的相对有效算法,包括随机算法和确定算法.目前,最好算法的时间复杂度不超过O（（2-2/k）ⁿ）,当k=3时,最好算法时间复杂度为O（1.308ⁿ）.而对于更一般的与子句长度k无关的SAT问题,很少有文献涉及.引入了一类可分离SAT问题,即3-正则可分离可满足性问题（3-RSSAT）,证明了3-RSSAT是NP完全问题,给出了一般SAT问题3-正则可分离性的O（1.890ⁿ）判定算法.然后,利用矩阵相乘算法的研究成果,给出了3-RSSAT问题的O（1.890ⁿ）精确算法,该算法与子句长度无关.