由鸽巢原理定义的鸽巢公式pHn+1 n是著名的消解难例之一,研究该公式的结构和性质有助于其他难例的构造.证明了pHn+1 n是一个极小不可满足公式,根据其极小不可满足性,给出了最大可满足真值指派的两种标准形式,Haken关于pHn+1 n的难解证明用到了其中一种标准形式.公式pHn+1 n具有良好的子结构同构性质,如果DPLL算法中允许使用同构规则,则存在PHn+1 n的反驳证明,其复杂性可以降至O(n3).%The pigeon-hole formula PHnn+2, defined from the pigeon hole principles, is one of the hardest examples on resolution. The research of the formula's constructions and properties is helpful for constructing other hard examples. It is shown that PHInn+1 is a minimal unsatisfiable formula. The two normal forms of maximal satisfiable truth assignments for PHnn+1 are presented by the minimal unsatisfiability of PHnn+1, which one of normal forms is used in Haken's proof of hardness for PHnn+1. The formula PHnn+1 has well isomorphics properties on substructures. For the modified DPLL algorithm introduced by the isomorphism rule, the complexity of refutation proof of PHnn+1 can be reduced to O(n3).
展开▼
