极小不可满足公式的两个多项式时间可判定类

研究命题公式 (合取范式 )的极小不可满足性 .设公式F含有n +k个子句(n是F中所有变元的个数 ) ,其中包括子句x1∨…∨xn 和┐x1∨…∨┐xn,证明了当k≤ 4时 。