# 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 .

Download: |
PDF
Download (291kB) | Preview |
---|---|

Editorial actions: |
View Item (Login required) |

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 |