Abstract
The latest generation of SAT solvers (e.g. [10,7]) generally have three key features: randomization of variable selection, backtracking search, and some form of clause learning. We present a simple algorithm with these three features and prove that for instances with constant Δ (where Δ is the clause-to-variable ratio) the algorithm indeed has good worst-case performance, not only for computing SAT/UNSAT but more general properties as well, such as maximum satisfiability and counting the number of satisfying assignments. In general, the algorithm can determine any property that is computable via self-reductions on the formula.
One corollary of our findings is that for all fixed Δ and k ≥ 2, Max-k -SAT is solvable in O(c n) expected time for some c < 2, partially resolving a long-standing open problem in improved exponential time algorithms. For example, when Δ = 4.2 and k = 3, Max-k -SAT is solvable in O(1.8932n) worst-case expected time. We also improve the known time bounds for exact solution of #2SAT and #3SAT, and the bounds for k-SAT when k ≥ 5.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bansal, N., Raman, V.: Upper bounds for MaxSat: Further improved. In: Proc. of the 10th ISAAC (1999)
Dahllöf, V., Jonsson, P., Wahlstrm, M.: Counting Satisfying Assignments in 2-SAT and 3-SAT. In: Proc. of COCOON, pp. 535–543 (2002)
Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(1), 201–215 (1960)
Hirsch, E.A.: New worst-case upper bounds for SAT. Journal of Automated Reasoning, Special Issue II on Satisfiability in Year 2000 (2000); A preliminary version appeared in Proceedings of SODA 1998 (1998)
Hirsch, E.A.: Worst-case Time Bounds for MAX-k-SAT with respect to the Number of Variables Using Local Search. In: ICALP Workshop on Approximation and Randomized Algorithms in Communication Networks, pp. 69–76 (2000)
Hofmeister, T., Schoening, U., Schuler, R., Watanabe, O.: A probabilistic 3-SAT algorithm further improved. In: Proc. of STACS, pp. 192–202 (2002)
Lynce, I., Marques-Silva, J.: Complete unrestricted backtracking algorithms for satisfiability. In: Fifth International Symposium on the Theory and Applications of Satisfiability Testing (2002)
Monien, B., Speckenmeyer, E.: 3-satisfiability is testable in O(1.62r) steps, Bericht Nr. 3/1979, Reihe Theoretische Informatik, Universität-Gesamthochschule-Paderborn
Monien, B., Speckenmeyer, E.: Upper bounds for covering problems. Bericht Nr. 7/1980, Reihe Theoretische Informatik, Universität-Gesamthochschule-Paderborn
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. DAC 2001 (2001)
Paturi, R., Pudlak, P., Zane, F.: Satisfiability Coding Lemma. In: Proc. of the 38th IEEE FOCS, pp. 566–574 (1997)
Paturi, R., Pudlak, P., Saks, M.E., Zane, F.: An improved exponential-time algorithm for k-SAT. In: Proc. of the 39th IEEE FOCS, pp. 628–637 (1998)
Robson, M.: Algorithms for maximum independent sets. Journal of Algorithms 7(3), 425–440 (1986)
Schoening, U.: A probabilistic algorithm for k-SAT and constraint satisfaction problems. In: Proc. of the 40th IEEE FOCS, pp. 410–414 (1999)
Selman, B., Kautz, H., Cohen, B.: Local Search Strategies for Satisfiability Testing. Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge (1993)
Williams, R.: Algorithms for quantified Boolean formulas. In: Proc. ACM-SIAM SODA, pp. 299–307 (2002)
Williams, R., Gomes, C., Selman, B.: Backdoors To Typical Case Complexity. To appear in Proc. of IJCAI (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Williams, R. (2004). On Computing k-CNF Formula Properties. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive