Key Words And Minimal Unsatisfiable Formulas

A literal is a propositional variable or a negated propositional variable. A clause C is a disjunction of literals and a formula is a conjunction of clauses. The formula F is satisfiable if there exits a truth assignment which satisfies F, otherwise it is unsatisfiable. Determining whether a formula is satisfiable is SAT problem. An important algorithm solving SAT problem is DPLL algorithm. A formula F is called minimal unsatisfiable (MU) if F is unsatisfiable and F - {C} is satisfiable for any clause C of F . German scholar H.K.Bǖning and O .Kullmann and others in this area have done a lot of important work. Structure and nature of MU formula will help determine SAT algorithm research.For 3-SAT, experimental results have shown that randomly generated 3-SATinstances of M clauses and N variables with the propertyα=M/N= 4.26 =α_care hard to solve. Furthermore, instances withα<α_c orα>α_c seem to berelatively easy to solve. This easy-hard-easy effect is characterized as the phase transition of SAT , which is originally the concept of physics. Based on phase transition phenomenon, in 1999, Monasson introduced the concept of the backbone of a SAT formula. The backbone corresponds to the set of variables having a fixed truth value in all assignments satisfying the maximum number of clause of a k -SAT formula. Two years later, Olivier Dubois defined a heuristic algorithm searching backbone of formula, but without theoretical studies.Based on heuristic algorithm, on the one hand, the paper defines the key literal of SAT formula, studies the property of the key literal, and designs an algorithm, an improving method of DPLL algorithm. On the other hand, using special structure of MU formula, the paper defines relative key literal of MU formula, studies the relation between relative key literal and MU formula, and proves that only using key literal rule and pure literal rule, can make the MaxSAT of MU(1) formulas empty in O(n~2).