Abstract:The pigeon-hole formula PH_nⁿ⁺¹, 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 PH_nⁿ⁺¹ is a minimal unsatisfiable formula. The two normal forms of maximal satisfiable truth assignments for PH_nⁿ⁺¹ are presented by the minimal unsatisfiability of PH_nⁿ⁺¹, which one of normal forms is used in Haken’s proof of hardness for PH_nⁿ⁺¹. The formula PH_nⁿ⁺¹ has well isomorphics properties on substructures. For the modified DPLL algorithm introduced by the isomorphism rule, the complexity of refutation proof of PH_nⁿ⁺¹ can be reduced to O(n³).