摘要
合取范式(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.
出处
《软件学报》
EI
CSCD
北大核心
2006年第5期1204-1212,共9页
Journal of Software
基金
国家自然科学基金
贵州省高层次人才科研条件特助基金
贵州省省长基金~~
关键词
极小不可满足公式
问题
多项式归约
NP-完全
公式构造
minimal unsatisfiable formula
SAT-problem
polynomiaUy reduction
NP-completeness
construction offormula
