Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable (Q557836): Difference between revisions
From MaRDI portal
Created a new Item |
ReferenceBot (talk | contribs) Changed an Item |
||
(4 intermediate revisions by 4 users not shown) | |||
Property / 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. | |||
Property / 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. / rank | |||
Normal rank | |||
Property / reviewed by | |||
Property / reviewed by: Roberto Solis-Oba / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68Q25 / rank | |||
Normal rank | |||
Property / Mathematics Subject Classification ID | |||
Property / Mathematics Subject Classification ID: 68T20 / rank | |||
Normal rank | |||
Property / zbMATH DE Number | |||
Property / zbMATH DE Number: 2184061 / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
unsatisfiable formulas | |||
Property / zbMATH Keywords: unsatisfiable formulas / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
integer sequences | |||
Property / zbMATH Keywords: integer sequences / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
complexity | |||
Property / zbMATH Keywords: complexity / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
\((k,s)\)-SAT | |||
Property / zbMATH Keywords: \((k,s)\)-SAT / rank | |||
Normal rank | |||
Property / zbMATH Keywords | |||
NP-completeness | |||
Property / zbMATH Keywords: NP-completeness / rank | |||
Normal rank | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/j.tcs.2005.02.004 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1979831715 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the r,s-SAT satisfiability problem and a conjecture of Tovey / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A Note on Unsatisfiable <i>k</i>-CNF Formulas with Few Occurrences per Variable / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: On the structure of some classes of minimal unsatisfiable formulas / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Satisfiability of co-nested formulas / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: DNF tautologies with a limited number of occurrences of every variable / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Homomorphisms of conjunctive normal forms. / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A simplified NP-complete satisfiability problem / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 13:08, 10 June 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable |
scientific article |
Statements
Computing unsatisfiable \(k\)-SAT instances with few occurrences per variable (English)
0 references
30 June 2005
0 references
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.
0 references
unsatisfiable formulas
0 references
integer sequences
0 references
complexity
0 references
\((k,s)\)-SAT
0 references
NP-completeness
0 references