The minimal unsatisfiability problem is considered of the prepositional formulas in CNF which in the case of variablesx 1,?,x n consist ofn +k clauses including it,x 1 V ? Vx n and ?x 1 V ? V ?x n It is shown that whe...The minimal unsatisfiability problem is considered of the prepositional formulas in CNF which in the case of variablesx 1,?,x n consist ofn +k clauses including it,x 1 V ? Vx n and ?x 1 V ? V ?x n It is shown that whenk ?4 the minimal unsatisfiability problem can be solved in polynomial time.展开更多
合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,...合取范式(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-完全的.展开更多
通过一个适当的归约变换,可以将一个CNF(conjunctive normal form)公式变换为另一个具有某种特殊结构或性质的公式,使两者具有相同的可满足性。带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果,可以用于研究公式的可满...通过一个适当的归约变换,可以将一个CNF(conjunctive normal form)公式变换为另一个具有某种特殊结构或性质的公式,使两者具有相同的可满足性。带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果,可以用于研究公式的可满足性和计算复杂性。极小不可满足公式具有一个临界特征,公式本身不可满足,从原始公式中删去任意一个子句后得到的公式可满足。借助此临界特性,给出了一个从3-CNF公式到正则(3,4)-CNF公式的多项式归约转换。这里,正则(3,4)-CNF公式是指公式中每个子句的长度恰为3,每个变元出现的次数恰为4。因此,正则(3,4)-SAT问题是一个NP-完全问题,并且MAX(3,4)-SAT是不可近似问题。展开更多
基金Project supported by the National Natural Science Foundation of China (Grant No. 19771045)Nationl High-Tech R&D Project (863) (Grant No. 863-306-ET06-01-2).
文摘The minimal unsatisfiability problem is considered of the prepositional formulas in CNF which in the case of variablesx 1,?,x n consist ofn +k clauses including it,x 1 V ? Vx n and ?x 1 V ? V ?x n It is shown that whenk ?4 the minimal unsatisfiability problem can be solved in polynomial time.
基金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-完全的.
基金Supported by the National Natural Science Foundation of Chinaunder GrantNos.60425206,60773104,60403016,60633010(国家自然科学基金)in Partby the Jiangsu Planned Projects for Postdoctoral Research Funds of Chinaunder GrantNo.0701003B(江苏省博士后科研资助计划)
文摘通过一个适当的归约变换,可以将一个CNF(conjunctive normal form)公式变换为另一个具有某种特殊结构或性质的公式,使两者具有相同的可满足性。带有正则结构的CNF公式的因子图在图论中具有某些良好的性质和结果,可以用于研究公式的可满足性和计算复杂性。极小不可满足公式具有一个临界特征,公式本身不可满足,从原始公式中删去任意一个子句后得到的公式可满足。借助此临界特性,给出了一个从3-CNF公式到正则(3,4)-CNF公式的多项式归约转换。这里,正则(3,4)-CNF公式是指公式中每个子句的长度恰为3,每个变元出现的次数恰为4。因此,正则(3,4)-SAT问题是一个NP-完全问题,并且MAX(3,4)-SAT是不可近似问题。
