Clause Shortening Combined with Pruning Yields a New Upper Bound for Deterministic SAT Algorithms

1. Bollobás, B.: Random Graphs, 2nd edn. Cambridge University Press, Cambridge (2001)

   MATH  Google Scholar 

2. Brueggemann, T., Kern, W.: An improved local search algorithm for 3-SAT. Theoretical Computer Science 329(1-3), 303–313 (2004)

   Article  MATH  MathSciNet  Google Scholar 

3. Dantsin, E., Goerdt, A., Hirsch, E.A., Kannan, R., Kleinberg, J., Papadimitriou, C., Raghavan, P., Schöning, U.: A deterministic (2 − 2/(k + 1))ⁿ algorithm for k-SAT based on local search. Theoretical Computer Science 289(1), 69–83 (2002)

   Article  MATH  MathSciNet  Google Scholar 

4. 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)

   Chapter  Google Scholar 

5. 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. 80–88. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

6. Dantsin, E., Wolpert, A.: A faster clause-shortening algorithm for SAT with no restriction on clause length. Journal on Satisfiability, Boolean Modeling and Computation 1, 49–60 (2005)

   Google Scholar 

7. Iwama, K., Tamaki, S.: Improved upper bounds for 3-SAT. In: Proceedings of the 15th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, January 2004, p. 328 (2004)

   Google Scholar 

8. Paturi, R., Pudlák, P., Saks, M.E., Zane, F.: An improved exponential-time algorithm for k-SAT. In: Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1998, pp. 628–637 (1998)

   Google Scholar 

9. Paturi, R., Pudlák, P., Zane, F.: Satisfiability coding lemma. In: Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1997, pp. 566–574 (1997)

   Google Scholar 

10. Pudlák, P.: Satisfiability – algorithms and logic. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 129–141. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

11. Schöning, U.: A probabilistic algorithm for k-SAT and constraint satisfaction problems. In: Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science, FOCS 1999, pp. 410–414 (1999)

    Google Scholar 

12. Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. Journal of Algorithms 54(1), 40–44 (2003), A preliminary version appeared as a technical report in 2003

    Google Scholar 

13. Stanley, R.P.: Enumerative Combinatorics, vol. 1. Wadsworth & Brooks/Cole (1986)

    Google Scholar 

Download references