Abstract
We present an algorithm that decides the satisfiability of a formula F on CNF form in time O(1.1279(d − 2)n), if F has at most d occurrences per variable or if F has an average of d occurrences per variable and no variable occurs only once. For d ≤ 4, this is better than previous results. This is the first published algorithm that is explicitly constructed to be efficient for cases with a low number of occurrences per variable. Previous algorithms that are applicable to this case exist, but as these are designed for other (more general, or simply different) cases, their performance guarantees for this case are weaker.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Brueggemann, T., Kern, W.: An improved deterministic local search algorithm for 3-SAT. Theoretical Computer Science 329(1–3), 303–313 (2004)
Chen, J., Kanj, I.A., Xia, G.: Labeled search trees and amortized analysis: Improved upper bounds for NP-hard problems. In: Ibaraki, T., Katoh, N., Ono, H. (eds.) ISAAC 2003. LNCS, vol. 2906, pp. 148–157. Springer, Heidelberg (2003)
Dahllöf, V., Jonsson, P., Wahlström, M.: Counting models for 2SAT and 3SAT formulae. Theoretical Computer Science 332(1-3), 265–291 (2005)
Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J.M., Papadimitriou, C.H., Raghavan, P., Schöning, U.: A deterministic (2 − 2/(k + 1))n algorithm for k-SAT based on local search. Theoretical Computer Science 289(1), 69–83 (2002)
Dantsin, E., Hirsch, E.A., Wolpert, A.: Algorithms for SAT based on search in Hamming balls. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 141–151. Springer, Heidelberg (2004)
Dantsin, E., Wolpert, A.: Derandomization of Schuler’s algorithm for SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 69–75. Springer, Heidelberg (2005)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960)
Eppstein, D.: Improved algorithms for 3-coloring, 3-edge-coloring, and constraint satisfaction. In: Proceedings of the Twelfth Annual Symposium on Discrete Algorithms (SODA 2001), pp. 329–337 (2001)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, New York (1979)
Hirsch, E.A.: New worst-case upper bounds for SAT. Journal of Automated Reasoning 24(4), 397–420 (2000)
Iwama, K., Tamaki, S.: Improved upper bounds for 3-SAT. In: Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2004), p. 328 (2004)
Purdom Jr., P.W.: Solving satisfiability with less searching. IEEE Transactions on Pattern Analysis and Machine Intelligence PAMI-6, 510–513 (1984)
Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science 223, 1–72 (1999)
Schöning, U.: A probabilistic algorithm for k-SAT based on limited local search and restart. Algorithmica 32(4), 615–623 (2002)
Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. Journal of Algorithms 54(1), 40–44 (2004)
Szeider, S.: Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable. In: Warnow, T.J., Zhu, B. (eds.) COCOON 2003. LNCS, vol. 2697, pp. 548–558. Springer, Heidelberg (2003)
Tovey, C.A.: A simplified NP-complete satisfiability problem. Discrete Applied Mathematics 8, 85–89 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wahlström, M. (2005). Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_23
Download citation
DOI: https://doi.org/10.1007/11499107_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)