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

Applications of Minimal Unsatisfiable Formulas to Polynomially Reduction for Formulas

作　　者：许道云[1] 

机构地区：[1]贵州大学计算机科学系,贵州贵阳550025

出　　处：《软件学报》2006年第5期1204-1212,共9页Journal of Software

基　　金：国家自然科学基金;贵州省高层次人才科研条件特助基金;贵州省省长基金~~

摘　　要：合取范式(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)的子句,仅需引入???2l???个新变元.并且,给出了CNF到(r,s)-CNF公式转换以及(r,s)-CNF中不可满足公式构造的原理和方法.A conjunctive normal form （CNF） formula F is minimal unsatisfiable if F is unsatisfiable and the resulting formula removing any clause from F is satisfiable. （r,s）-CNF is a subclass of CNF in which each clause of formula has exactly r distinct literals and every variable occurs at most s times. The corresponding satisfiable problem （r,s）-SAT means that the instances are restricted in （r,s）-CNE For positive integer r≥3, there exists a critical functionf（r） such that all formulas in （r,f（r））-CNF are satisfiable, but （r,f（r）＋1）-SAT is already NP-Complete It is open whether or not the function f is computable. One can only estimate some bounds of fir） except for f（3）=3 and f（4）=4. In this paper, the applications of minimal unsatisfiable formulas are described for transformations between CNF formulas. A new algorithm is presented to introduce less new variables in transformation from CNF to 3-CNF, which for clauses with length/（〉3） only [l/2] new variables are introduced. The principle and method for transforming CNF to （r,s）-CNF and constructing unsatisfiable formulas in （r,s）-CNF are presented.

关 键 词：极小不可满足公式 问题 多项式归约 NP-完全 公式构造 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]