HITMU(2)的结构和复杂度

The Structure and Complexity of HIT—MU(2)

SAT问题(可满足性问题)是计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向. 本文主要利用1(,)*-消解和分裂方法研究了差为2的碰撞极小不可满足公式集()2(MUHIT-)的结构和复杂度.此前,只有G.Davydov, I.Davydova 和H.Kleine Büning对)1(MU和)2(MU的结构和复杂度得出了较好的结果.

SAT Problem is the core problem in computer science. There are many ways to research intoSAT Problem. Using the properties of minimal unsatisfiable formulas to study SAT Problem is a new hot research way at present. In this paper, the structure and complexity of hitting unsatisfiable formulas with deficiency 2 ()2(MUHIT-) are studied by 1(,)*-resolution and splitting technique. Before, only G.Davydov, I.Davydova and H.Kleine Büning derived good results from the structure and complexity of )1(MU and )2(MU.