可满足实例的归结复杂度  

Resolution complexity of satisfiability instances

作　　者：沈静[1] 梅丹[1] 

机构地区：[1]海军工程大学应用数学系,武汉430033

出　　处：《计算机工程与应用》2014年第22期69-72,共4页Computer Engineering and Applications

基　　金：国家自然科学基金(No.11171370)

摘　　要：GRB模型是一种随机约束满足问题模型,此模型具有精确的可满足相变现象。针对实验中出现的GRB模型在相变区域产生的可满足实例都是难解的现象,利用子句宽度和归结复杂度的关系证明了GRB模型在相变点附近产生的可满足实例对于树型归结证明具有指数下界。因此从理论上证明了在相变区域产生的可满足实例对基于归结的算法是难解的。The model GRB is a random model of constraint satisfaction problem, and it exhibits exact solubility phase transitions. For the experimental results that the satisfiability instances in the phase transition region are hard to solve, it uses the relation between the clause width and the resolution complexity to prove that almost all satisfiability instances of the model GRB have no tree-like resolution proofs of length less than exponential size. Therefore it shows theoretically that the satisfiability instances in the phase transition region are hard for the algorithms based on resolution.

关 键 词：归结复杂度 约束满足问题 可满足相变 

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