The Existence Of NT-HIT Formula

The satisfiable(SAT) problem plays an important role in artificial intelligence ,machine learning, mathematical logic, VLSI design and detection other areas. It lies at the every heart of a family of NP- complete problems, and is important to both computer science and practical applications.Research on the minimal unsatisfiable formula is a hot topic on SAT problem that begins to surface in recent years. A formula F is minimal unsatisfiable(MU) if F is unsatisfiable and F ^{C} is satisfiable for any clause C of F . A powerful for investigating the structure of minimal unsatisfiable formulas is splitting. We take a variable x, assign truth x = 0 and x -1 ,and consider the resulting formulas. For a minimal unsatisfiable the result formulas contain minimal unsatisfiable formulas. In particular, based on such a splitting induction proofs can be performed and characterization for some some classes of formulas can be established.In[13], Hans Kleine Buning obtains the result that K^* is closed under splitting, and leaves two open problems: (1)for any formula F∈NT -HIT(1), if there exists a literal L occurring exactly once in F .(2) for any k ≥ 2 ,if the set NT -HIT(k) is an empty set.Based on the conditions of NT - HIT formula, we construct formula H_n,m such that H_n,m is satisfiable if and only if there exists a NT - HIT formula with n variables and m clauses. By the properties of H_n,m, we prove that for any F∈ NT-HIT(1) there exists a literal L occurring exactly once in F ,and show that F ∈ NT -HIT(k) is an empty set for k ≥2 .Thus we solve positively two open problems.NT -HIT is an important class of propositional formula. The construction of H_n,m formula not only solve positively two open problems that have been puzzled the computer scientists for a long time, but also establish the characterization and structure of NT - HIT completely.