Resolution Tunnels for Improved SAT Solver Performance

1. Akers, S.B.: Binary decision diagrams. IEEE Transactions on Computers C-27(6), 509–516 (1978)

   Article  MATH  Google Scholar 

2. Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Proc. 37th Annual Symposium on Foundations of Computer Science, pp. 274–282 (1996)

   Google Scholar 

3. Beame, P., Karp, R.M., Pitassi, T., Saks, M.: On the complexity of unsatisfiability proofs for random k-CNF formulas. In: Proc. 30th Annual Symposium on the Theory of Computing, pp. 561–571 (1998)

   Google Scholar 

4. Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. Journal of the Association for Computing Machinery 48, 149–169 (2001)

   MATH  MathSciNet  Google Scholar 

5. Brace, K.S., Rudell, R.R., Bryant, R.E.: Efficient implementation of a BDD package. In: Proc. 27th ACM/IEEE Design Automation Conf., pp. 40–45 (1990)

   Google Scholar 

6. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp. C-35(8), 677–691 (1986)

   Article  MATH  Google Scholar 

7. Burch, J., Clark, E., Long, D.: Symbolic model checking with partitioned transitions relations. In: Halaas, A., Denyer, P.B. (eds.) Intnl. Conf. on VLSI. IFIP Transactions, pp. 49–58. North-Holland, Amsterdam (1991)

   Google Scholar 

8. Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the Association for Computing Machinery 35, 759–768 (1988)

   MATH  MathSciNet  Google Scholar 

9. Cooke, M.: Van der Waerden numbers, Available from http://home.comcast.net/~rm_cooke/vdw.html

10. Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the Association of Computing Machinery 5, 394–397 (1962)

    MATH  MathSciNet  Google Scholar 

11. Dransfield, M.R., Liu, L., Marek, V., Truszczynski, M.: Using Answer-Set Programming to study van der Waerden numbers. Logic and Artificial Intelligence Laboratory, Computer Science Department, College of Enginnering, University of Kentucky (September 2004), Available from http://cs.engr.uky.edu/ai/vdw/

12. Dransfield, M., Bryant, R.E.: Using ordered binary decision diagrams to solve highly structured satisfiability problems. Unpublished technical report CMU-CS-1996, Carnegie Mellon University (1996)

    Google Scholar 

13. Galil, Z.: On resolution with clauses of bounded size. SIAM Journal on Computing 6, 444–459 (1977)

    Article  MATH  MathSciNet  Google Scholar 

14. Gent, I.P., Walsh, T.: Towards an understanding of hill-climbing procedures for SAT. In: Proc. 11th National Conference on Artificial Intelligence, pp. 28–33 (1993)

    Google Scholar 

15. Groote, J.F.: Hiding propositional constants in BDDs. Logic Group Preprint Series 120, Utrecht University (1994)

    Google Scholar 

16. Gu, J.: Efficient local search for very large-scale satisfiability problems. ACM SIGART Bulletin 3(1), 8–12 (1992)

    Article  Google Scholar 

17. Gu, J., Purdom, P.W., Franco, J., Wah, J.: Algorithms for the Satisfiability problem: a survey. DIMACS Series on Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 19–151 (1997)

    Google Scholar 

18. Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297–308 (1985)

    Article  MATH  MathSciNet  Google Scholar 

19. Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell System Technical Journal 38, 985–999 (1959)

    MathSciNet  Google Scholar 

20. McAllester, D., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: Proc. International Joint Conference on Artificial Intelligence, pp. 321–326 (1997)

    Google Scholar 

21. Monien, B., Speckenmeyer, E.: Solving satisfiability in less than 2ⁿ steps. Discrete Applied Mathematics 10, 117–133 (1983)

    MathSciNet  Google Scholar 

22. Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12, 23–41 (1965)

    Article  MATH  Google Scholar 

23. Pan, G., Vardi, M.Y.: Search vs. symbolic techniques in satisfiability solving. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 235–250. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

24. San Miguel Aguirre, A., Vardi, M.Y.: Random 3-SAT and BDDs: The plot thickens further. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 121–136. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

25. Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. 12th National Conference on Artificial Intelligence, pp. 337–343 (1994)

    Google Scholar 

26. Somenzi, F.: Colorado University Decision Diagram package, Available from http://vlsi.colorado.edu/~fabio/CUDD/

27. Song, H.Y., Golomb, S.W., Taylor, H.: Progressions in Every Two-coloration of Z _n . Journal of Combinatorial Theory, Series A 61(2), 211–221 (1992)

    Article  MATH  MathSciNet  Google Scholar 

28. Rabung, J.R.: Some Progression-Free Partitions Constructed Using Folkman’s Method. Canadian Mathematical Bulletin 22(1), 87–91 (1979)

    Article  MATH  MathSciNet  Google Scholar 

29. Urquhart, A.: Hard examples for resolution. Journal of the Association for Computing Machinery 34, 209–219 (1987)

    MATH  MathSciNet  Google Scholar 

30. Van der Waerden, B.L.: Beweis einer Baudetschen Veermutung. Nieuw Archief voor Wiskunde 15, 212–216 (1927)

    Google Scholar 

31. Weaver, S.A., Franco, J., Schlipf, J.S.: Extending Existential Quantification in Conjunctions of BDDs. University of Cincinnati Technical Report

    Google Scholar 

32. Weisstein, E.W., et al.: van der Waerden Number, From MathWorld–A Wolfram Web Resource, http://mathworld.wolfram.com/vanderWaerdenNumber.html

Download references