k-LSAT is NP-Complete for k≥3

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[1], and for the class LCNF of linear formulas, 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 NP-completeness of the decision problem LSAT≥k is closely relevant to whether or not there exists an unsatisfiable formula in LCNF≥k, i.e., the NP-completness 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≥3 and LCNF≥4 contain 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.