Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable
type: Item
instance of: scholarly article
title: Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable
zbMATH Open document ID: 1087.68042
author: Shlomo Hoory
author: Stefan Szeider
published in: Theoretical Computer Science
publication date: 2005-06-30T00:00:00Z
review text: Let \((k,s)\)-CNF be the set of Boolean formulas in which every clause has exactly \(k\) different literals and each Boolean variable occurs in at most \(s\) clauses. Then, \((k,s)\)-SAT is the satisfiability problem restricted to \((k,s)\)-CNF. It was shown by \textit{J. Kratochvíl, P. Savický} and \textit{Z. Tuza} [SIAM J. Comput. 22, 203--210 (1993; Zbl 0767.68057)] that for every \(k \geq 3\) there is an integer \(f(k)\) such that all formulas in \((k,f(k))\)-CNF are satisfiable and \((k,f(k)+1)\)-SAT is NP-complete. It is not known whether the function \(f\) is computable, but several asymptotic upper and lower bounds for \(f\) have been published in the literature. Since most formulas arising in practice have clauses with few literals, there has been a lot of interest in computing good bounds for \(f(k)\) for small values of \(k\). In the paper the authors derive bounds for \(f(k)\), \(k = 4, 5, 6, 7, 8, 9\), that improve on the previously best known bounds presented by \textit{P. Berman, M. Karpinksi} and \textit{A. D. Scott} [Approximation hardness and satisfiability of bounded occurrence instances of SAT, Technical Report TR03-022, Electronic Colloquium on Computational Complexity (2003)]. The above bounds are obtained though a novel, simple technique for generating unsatisfiable \((k,s)\)-CNF formulas. This technique only considers MU(1) formulas: minimal unsatisfiable formulas (where the removal of any clause makes the formula satisfiable) with one more clause than the number of variables. The paper shows that the function \(f_1(k)\) giving the largest value such that \((k,f_1(k))\)-CNF \(\cap\) MU(1) \(\not = \emptyset\) is computable and it presents a saturation algorithm that computes this function in \(O(4^{k^2})\) time. The algorithm is based on the fact that finding unsatisfiable \((k,s)\)-CNF formulas in MU(1) is equivalent to a search problem on ordered integer sequences.
reviewed by: Roberto Solis-Oba
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68T20
zbMATH DE Number: 2184061
zbMATH Keywords: unsatisfiable formulas
zbMATH Keywords: integer sequences
zbMATH Keywords: complexity
zbMATH Keywords: \((k,s)\)-SAT
zbMATH Keywords: NP-completeness
MaRDI profile type: Publication
full work available at URL: j.tcs.2005.02.004
OpenAlex ID: W1979831715
cites work: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
cites work: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
cites work: On the r,s-SAT satisfiability problem and a conjecture of Tovey
cites work: A Note on Unsatisfiable k-CNF Formulas with Few Occurrences per Variable
cites work: On the structure of some classes of minimal unsatisfiable formulas
cites work: Satisfiability of co-nested formulas
cites work: DNF tautologies with a limited number of occurrences of every variable
cites work: Homomorphisms of conjunctive normal forms.
cites work: A simplified NP-complete satisfiability problem
DOI: 10.1016/J.TCS.2005.02.004
description: scientific article; zbMATH DE number 2184061