The Complexity Of Extending A Formula To A MU(1) Formula

SAT problem in classical logic means the satisfiability problem of boolean formulas. it is an essential problem of computer science. SAT problem belongs to the NP class, that is, theoretically it can't be solved in polynomial time and solving it exceeds the capability of modern computer. Therefore, SAT problem is the choke point in the development of computer science, computer scientists are trying to find various kinds of strategies and approaches to solve it all the while.Research on minimal unsatisfiable formula is a hot topic on SAT problem that begins to surface in recent years. A formula F in conjunctive normal form (CNF ) is a conjunction of finite clauses,A formula F is minimal unsatisfiable (MU) if F is unsatisfiable and F — {C} is satisfiable for any clause C of F. The deficiency of a formula F is defined as the margin between the number of clauses of F and the number of variables occurring in F, we denote MU(k) as the set of minimal unsatisfiable formulas with deficiency k ≥ 1. It is well known that F is not minimal unsatisfiable if k < 1.In this thesis, an algorithm for extending a satisfiable CNF formula to a MU(1) is presented. Concerning the extension problem, Kleine Buning.H and Zhao.X.S have obtained several results . They have concluded that the problem of extending a Horn formula to MU formula is solvable in polynomial time, and the problem of MU-EXT[ext = t] is D^p-hard, the problem MU-EXT[ext = 1] is in P^NP[logn], the problem MU-EXT[ext = t, defi = k] is solvable in polynomial time, where denote MU-EXT[ext = t,defi = k] = {F ∈ CNF|(?)G : F + G ∈ MU(k),var(G) (?) var(F), |G| = t}. In this paper, we will consider the problem that for a giver formula F(of cause F is satisfiable), whether there exist a formula G with var(G) C var(F) such that F + G ∈ MU(1).This is , we ignore the length of formula G and fixed k=1 in the problem MU - EXT[ext = t,defi = k]. Kleine Buning and Zhao.X.S. conjectured that for fixed t and k the problem MU — EXT[ext = t, defi = k] is solvable in polynomial time. Ignoring t will make problem more easy, we consider such a problem in this thesis.