k-LSAT(k≥3)是NP-完全的(英文)  被引量:5

k-LSAT is NP-Complete for k≥3

在线阅读下载全文

作  者:许道云[1] 邓天炎[1] 张庆顺[1] 

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

出  处:《软件学报》2008年第3期511-521,共11页Journal of Software

基  金:Supported by the National Natural Science Foundation of China under Grant Nos.10410638, 60310213 (国家自然科学基金)

摘  要:合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF≥k是子句长度大于或等于k的CNF公式子类,判定问题LSAT≥k的NP-完全性与LCNF≥k中是否含有不可满足公式密切相关.即LSAT≥k的NP-完全性取决于LCNF≥k是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF≥3和LCNF≥4中的不可满足公式,并提出公开问题:对于k≥5,LCNF≥k是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.A CNF formula F is linear if any distinct clauses in F contain at most one common variable. A CNF formula F is exact linear if any distinct clauses in F contain exactly one common variable. All exact linear formulas are satisfiable, and for the class LCNF of linear formulas, the decision problem LSAT remains NP-complete. For the subclasses LCNF≥k of LCNF, in which formulas have only clauses of length at least k, the NP-completeness of the decision problem LSAT≥k is closely relevant to whether or not there exists an unsatisfiable formula in LCNF≥k, i.e., the NP-completness of SAT for LCNF≥k (k≥3) is the question whether there exists an unsatisfiable formula in LCNF≥k. S. Porschen et al. have shown that both LCNF≥3 and LCNF≥4 contain unsatisfiable formulas by the constructions of hypergraphs and latin squares. It leaves the open question whether for each k≥5 there is an unsatisfiable formula in LCNF≥k. This paper presents a simple and general method to construct unsatisfiable formulas in k-LCNF for each k≥3 by the application of minimal unsatisfiable formulas to reductions for formulas. It is shown that for each k≥_3 there exists a minimal unsatisfiable formula in k-LCNF. Therefore, the stronger result is shown that k-LSAT is NP-complete for k≥3.

关 键 词:线性CNF公式 不可满足性 NP-完全性 极小不可满足公式 归约 

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

 

参考文献:

正在载入数据...

 

二级参考文献:

正在载入数据...

 

耦合文献:

正在载入数据...

 

引证文献:

正在载入数据...

 

二级引证文献:

正在载入数据...

 

同被引文献:

正在载入数据...

 

相关期刊文献:

正在载入数据...

相关的主题
相关的作者对象
相关的机构对象