论文部分内容阅读
一个合取范式(CNF)命题公式F称为极小不可满足公式,如果F不可满足,但从F中删去任何一个子句后得到一可满足公式。极小不可满足公式类记为MU,MU的判定问题是Dp-完全的,其中Dp是两个NP-问题之差的问题类。对于CNF公式F,我们记d(F)为F的子句数和变元数之差,MU(k)表示差为k的极小不可满足公式所构成的集合。对于固定的k,差为k的公式的满足性问题仍是NP-完全的。但可断言:差为k的公式的极小不可满足性问题可在多项式时间内被解决。
在第三章中,我们主要研究了HIT-MU(2),Unique-MU(2),MAX(2),MARG(2)和SYM-MU(2)的结构和复杂度,但MARG(2)的复杂度还未被解决。在结构方面,结果如下:HIT-MU(2)中的公式要么是在经过适当的改名和调整变元顺序后为F22或F22,要么是某一文字在其中仅出现一次的公式;MAX(2)中的公式要么是经过适当的改名和调整变元顺序后为F22,要么是某一文字在其中仅出现一次的公式;MARG(2)中的公式由F22和某一文字在其中仅出现一次的公式组成;Unique-MU(2)和SYM-MU(2)则仅含有一个公式F22。至于复杂度方面:HIT-MU(2)和MAX(2)可在时间O(n3)内被解决,Unique-MU(2)和SYM-MU(2)则可在线性时间内被解决。
在第四章中我们研究了HIT-MU,Unique-MU,MAX,MARG,SYM-MU,Dis-MU和CCNF之间的包含关系。其结果是:CCNF包含于HIT-MU,Unique-MU,MAX,MARG,SYM-MU和Dis-MU,HIT-MU包含于MAX,Dis-MU包含于Unique-MU,其它的包含关系都不成立。