| 摘要: |
| 合取范式(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中不可满足公式构造的原理和方法. |
| 关键词: 极小不可满足公式 问题 多项式归约 NP-完全 公式构造 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant No.60463001(国家自然科学基金);the Special Foundation for Improving Scientific Research Condition of Guizhou(贵州省高层次人才科研条件特助基金);the Special Foundation of Government of Guizhou Province(贵州省省长基金) |
|
| Applications of Minimal Unsatisfiable Formulas to Polynomially Reduction for Formulas |
|
XU Dao-Yun
|
| Abstract: |
| 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)-CNF. For positive integer r≥3, there exists a critical function f(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 f(r) 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 l(>3) only ??????2l 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. |
| Key words: minimal unsatisfiable formula SAT-problem polynomially reduction NP-completeness construction of formula |
