Abstract: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 distinet clauses in F contain exactly one conlrnon vailable.All exact linear formulas are satisfiable[1],and for the class LCNF of linear formulas,the decision problem LSAT remains NP-complete.For the subclasses LCNF≥kof LCNF,in which formulas have only clauses of length at least k,the NP-completeness of the decision problem LSAT≥kis closely relevant to whether or not there exists an unsatisfiable formula in LCNF≥k,i.e.,the NP-eompletness of SAT for LCNF≥k(k≥3)is the question whether there exists an unsatisfiable formula in LCNF≥k.S.Porschen et al.have shown that both LCNF≥3and LCNF≥4contain unsatisfiable formulas by the constructions of hypergraphs and latin squares.It leaves the open question whether for each k≥5 there is an unsatisfiable formula in LCNF≥k.This paper presents a simple and general method to construct unsatisfiable formulas in k-LCNF for each k≥3 by the application of minimal unsatisfiable formulas to reductions for formulas.It is shown that for each k≥3 there exists a minimal unsatisfiable formula in k-LCNF.Therefore,the stronger result is shown that k-LSAT is NP-complete for k≥3.