鸽巢公式的一些性质

由鸽巢原理定义的鸽巢公式PH nn+1是著名的消解难例之一,研究该公式的结构和性质有助于其他难例的构造.证明了PH nn+1是一个极小不可满足公式,根据其极小不可满足性,给出了最大可满足真值指派的两种标准形式,Haken关于PH nn+1的难解证明用到了其中一种标准形式.公式PH nn+1具有良好的子结构同构性质,如果DPLL算法中允许使用同构规则,则存在PH nn+1的反驳证明,其复杂性可以降至O(n3).