کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
420680 | 683968 | 2009 | 23 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: Linear CNF formulas and satisfiability Linear CNF formulas and satisfiability](/preview/png/420680.png)
In this paper, we study 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 NP-completeness of SAT for uniform linear classes in a resolution-based manner by constructing 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 rather dense, and significantly smaller unsatisfiable kk-uniform linear formulas, at least for the cases k=3,4k=3,4.
Journal: Discrete Applied Mathematics - Volume 157, Issue 5, 6 March 2009, Pages 1046–1068