Abstract: 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.

Key words: resolution complexity, constraint satisfaction problem（CSP）, solubility phase transition

摘要： GRB模型是一种随机约束满足问题模型，此模型具有精确的可满足相变现象。针对实验中出现的GRB模型在相变区域产生的可满足实例都是难解的现象，利用子句宽度和归结复杂度的关系证明了GRB模型在相变点附近产生的可满足实例对于树型归结证明具有指数下界。因此从理论上证明了在相变区域产生的可满足实例对基于归结的算法是难解的。

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