论文部分内容阅读
一个合取范式(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，其它的包含关系都不成立。