Universität zu Köln

Porschen, Stefan, Speckenmeyer, Ewald and Zhao, Xishun (2006). Linear CNF formulas and satisfiability. Working Paper.

Preview

PDF zaik2006-520.pdf - Draft Version Download (291kB) | Preview

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 .

Item Type:	Monograph (Working Paper)
Creators:	Creators Email ORCID ORCID Put Code Porschen, Stefan UNSPECIFIED UNSPECIFIED UNSPECIFIED Speckenmeyer, Ewald UNSPECIFIED UNSPECIFIED UNSPECIFIED Zhao, Xishun UNSPECIFIED UNSPECIFIED UNSPECIFIED
URN:	urn:nbn:de:hbz:38-548989
Date:	2006
Language:	English
Faculty:	Faculty of Mathematics and Natural Sciences
Divisions:	Faculty of Mathematics and Natural Sciences > Department of Mathematics and Computer Science > Institute of Computer Science
Subjects:	Data processing Computer science
Refereed:	No
URI:	http://kups.ub.uni-koeln.de/id/eprint/54898