Linear CNF formulas and satisfiability

Porschen, Stefan and Speckenmeyer, Ewald and Zhao, Xishun (2006) Linear CNF formulas and satisfiability.
Technical Report , 37 p.

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 .


Actions:
Download: [img] PDF
Download (291kB) | Preview
Editorial actions: View Item View Item (Login required)
Deposit Information:
ZAIK Number: zaik2006-520
Depositing User: Stefan Porschen
Date Deposited: 17 Apr 2007 00:00
Last Modified: 12 Jan 2012 10:05
URI: http://e-archive.informatik.uni-koeln.de/id/eprint/520