Linear Formula To Meet The Complexity Of The Decision Problem

The satisfiability problem (SAT for short) ,a major problem in computer science,which is the first NP -complete problem and the nucleus of the category of NP -complete problem.SAT problem is the set of satisfiable boolean formulas,which can be widely used in such fields as symbolic logic,artificial intelligence,constraint satisfaction problem,design and detection of VLSI integrate circuit,theories of computer science,computer vision,proof of machine theory,robot program,and machine learning.A CNF formula F is linear if any distinct clauses in F contain at most one common variable. A CNF formula F is exact linear if any distinct clauses in F contain exactly one common variable.All exact linear formulas are satisfiable([33]S. Porschen etc., 2006) ,and for the class of linear formulas LCNF ,the decision problem LSAT remains NP -complete .For the subclasses LCNF_≥k of LCNF ,in which formulas have only clauses of length at least k , the decision problem LSAT_≥k remains NP -complete if there exists an unsatisfiable formula in LCNF_≥k ([31,32]S. Porschen, E. Speckenmeyer, 2006) .Therefore, the NP -completeness of SAT for LCNF_≥k(k≥3) is the question whether there exists an unsatisfiable formula in LCNF_≥k .In ([31,32]S. Porschen, E. Speckenmeyer, 2006) ,it is shown that both LCNF_≥3 and LCNF_≥4 contain unsatisfiable formulas by the constructions of hypergraphs and latin spuares.It leaves the open question whether for each k≥5 there is an unsatisfiable formula in LCNF_≥k.Based on the structure and property of linear formulas, we present a algorithm which reduce a formula F to a linear formula F^lin in polynomial time of |F| . F is satisfiable if and only if F^lin is satisfiable . Further,we present a simple and general method to construct unsatisfiable formulas in k-LCNF , which formulas have every clauses of length k ,for each k≥3 by the application of minimal unsatisfiable formulas to reductions for formulas.We show for each k≥3 that there exists an minimal unsatisfiable formula in k - LCNF. Therefore,the stronger result is shown,which k-LSAT is NP -complete for k≥3.