MARG-MU(2)的结构和复杂度

The structure and complexity of MARG-MU(2)

SAT问题(可满足性问题)是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向。本文主要利用(1,*)-消解方法研究了差为2的边缘极小不可满足公式集(MARG-MU(2))的结构和复杂度:在结构方面,MARG-MU(2)中的公式要么是F22,要么是某一文字在其中仅出现一次的公式;在复杂度方面,如果MARG-MU(2)对(1,*)-消解封闭,则某个含有n个变元和n+2个子句的公式是否为MARG-MU(2)中的公式的问题可以在时间O(n3)内被判定。

SAT Problem is a core problem in theoretical computer science.There are many ways to research on SAT Problem.Using the properties of minimal unsatisfiable formulas to study SAT Problem is a new hot research field at present.In this paper,the structure and complexity of marginal minimal unsatisfiable formulas with deficiency 2(MARG-MU(2)) are studied by using(1,*),-resolution.Either(MARG-MU(2)) contains F22,or the formula occurres with literals exactly once in the structure.As to the complexity,if(MARG-MU(2)) is closed under(1,*),the problem whether a formula F over n variables and n+2 clauses is in(MARG-MU(2)) can be solved in O(n3) time complexity.