Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable (Q557836)

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.