"Linear CNF formulas and satisfiability"
Technical report by Stefan Porschen, Ewald Speckenmeyer, Xishun Zhao, available as BibTeX Source and in portable document format.
Zentrum für Angewandte Informatik Köln, Lehrstuhl Speckenmeyer
Preprint Key:	zaik2006-520
Keywords:	finite projective plane, la-tin squ-are, linear CNF formula, NP-completeness, resolution proof, Satisfiability
MSC codes:	03B05, 05C69, 05C85, 68Q25
This technical report has 37 pages, was written in September 2006, it has not been published.
Abstract:	In this paper, we study {em linear} CNF formulas generalizing linear hypergraphs under combinatorial and complexity theoretical aspects w.r.t. SAT. We establish NP-completeness of SAT for the unrestricted linear formula class, and we show the equivalence of NP-completeness of restricted uniform linear formula classes w.r.t. SAT and the existence of unsatisfiable uniform linear witness formulas. On that basis we prove the NP-completeness of SAT for the uniform linear classes in a proof-theoretic manner by constructing however large-sized formulas. Interested in small witness formulas, we exhibit some combinatorial features of linear hypergraphs closely related to latin squares and finite projective planes helping to construct somehow dense, and significantly smaller unsatisfiable k-uniform linear formulas, at least for the cases k=3,4.