Advertisement

Random 3-SAT and BDDs: The Plot Thickens Further

  • Alfonso San Miguel Aguirre
  • MosheY. Vardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2239)

Abstract

This paper contains an experimental study of the impact of the construction strategy of reduced, ordered binary decision diagrams (ROBDDs) on the average-case computational complexity of random 3-SAT, using the CUDD package.We study the variation of median running times for a large collection of random 3-SAT problems as a function of the density as well as the order (number of variables) of the instances.We used ROBDD-based pure SAT-solving algorithms, which we obtained by an aggressive application of existential quantification, augmented by several heuristic optimizations. Our main finding is that our algorithms display an “easy-hard-less-hard” pattern that is quite similar to that observed earlier for search-based solvers. When we start with low-density instances and then increase the density, we go from a region of polynomial running time, to a region of exponential running time, where the exponent first increases and then decreases as a function of the density. The locations of both transitions, from polynomial to exponential and from increasing to decreasing exponent, are algorithm dependent. In particular, the running time peak is quite independent from the crossover density of 4.26 (where the probability of satisfiability declines precipitously); it occurs at density 3.8 for one algorithm and at density 2.3 for for another, demonstrating that the correlation between the crossover density and computational hardness is algorithm dependent.

Keywords

Boolean Function Binary Decision Diagram Symbolic Model Check Input Formula Ordered Binary Decision Diagram 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    D. Achlioptas. Setting two variables at a time yields a new lower bound for random 3-SAT. In Proc. 32th ACM Symp. on Theory of Computing, pages 28–37, 2000.Google Scholar
  2. 2.
    J. Balcazar. Self-reducibility. Journal of Computer and System Sciences, 41(3):367–388, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    P. Beame, R. M. Karp, T. Pitassi, and M. E. Saks. On the complexity of unsatisfiability proofs for random k-CNF formulas. In Proc. 30th ACM Symp. on Theory of Computing, pages 561–571, 1998.Google Scholar
  4. 4.
    A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. 36th Conf. on Design Automation, pages 317–320, 1999.Google Scholar
  5. 5.
    M. Block, C. Gröpl, H. Preu\, H. L. Proömel, and A. Srivastav. Efficient ordering of state variables and transition relation partitions in symbolic model checking. Technical report, Institute of Informatics, Humboldt University of Berlin, 1997.Google Scholar
  6. 6.
    F. Bouquet. Gestion de la dynamicité et énumération d’implicants premiers: une approche fondée sur les Diagrammes de Décision Binaire. PhD thesis, Université de Provence, France, 1999.Google Scholar
  7. 7.
    R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Computers, 35(8):677–691, 1986.zbMATHCrossRefGoogle Scholar
  8. 8.
    J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In Proc. IFIP TC10/WG 10.5 Int’l Conf. on Very Large Scale Integration, Edinburgh, Scotland (VLSI’91), pages 49–58, 1991.Google Scholar
  9. 9.
    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    P. Chatalic and L. Simon. The old Davis-Putnam procedure meets ZBDDs. In D. McAllester, editor, 17th Int’l Conf. on Automated Deduction (CADE’17), volume 1831 of Lecture Notes in Artificial Intelligence, pages 449–454, 2000.Google Scholar
  11. 11.
    P. Cheeseman, B. Kanefsky, and W. M. Taylor. Where the really hard problems are. In Proc. 12th Int’l Joint Conf. on Artificial Intelligence (IJCAI’ 91), pages 331–337, 1991.Google Scholar
  12. 12.
    V. Chvátal and E. Szemerédi. Many hard examples for resolution. J. of the ACM, 35(4):759–768, 1988.zbMATHCrossRefGoogle Scholar
  13. 13.
    C. Coarfa, D. D. Demopolous, A. San Miguel Aguirre, D. Subramanian, and M. Y. Vardi. Random 3-SAT: The plot thickens. In R. Dechter, editor, Proc. Principles and Practice of Constraint Programming (CP’2000), Lecture Notes in Computer Science 1894, pages 143–159, 2000.Google Scholar
  14. 14.
    S. Cocco and R. Monasson. Trajectories in phase diagrams, growth processes and computational complexity: how search algorithms solve the 3-Satisfiability problem. Phys. Rev. Lett., 86:1654–1657, 2001.CrossRefGoogle Scholar
  15. 15.
    J. M. Crawford and L. D. Auton. Experimental results on the crossover point in random 3-SAT. Artificial Intelligence, 81(1–2):31–57, 1996.CrossRefMathSciNetGoogle Scholar
  16. 16.
    M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Comm. of the ACM, 5:394–397, 1962.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    O. Dubois, Y. Boufkhad, and J. Mandler. Typical random 3-SAT formulae and the satisfiability threshold. In Proc. 11th Annual ACM-SIAM Symp. on Discrete Algorithms, pages 126–127, 2000.Google Scholar
  18. 18.
    E. Friedgut. Necessary and sufficient conditions for sharp threshold of graph properties and the k-SAT problem. J. Amer. Math. Soc., 12:1017–1054, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    D. Geist and H. Beer. Efficient model checking by automated ordering of transition relation partitions. In Proc. 6th Int’l Conf. on Computer Aided Verification (CAV’ 94), pages 299–310, 1994.Google Scholar
  20. 20.
    I. P. Gent and T. Walsh. Easy problems are sometimes hard. Artificial Intelligence, 70(1–2):335–345, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    J. F. Groote. Hiding propositional constants in BDDs. Formal Methods in System Design, 8:91–96, 1996.CrossRefGoogle Scholar
  22. 22.
    J. F. Groote and H. Zantema. Resolution and binary decision diagrams cannot simulate each other polynomially. Technical report, Department of Computer Science, Utrecht University, 2000. Technical Report UU-CS-2000-14.Google Scholar
  23. 23.
    T. Hogg and C. P. Williams. The hardest constraint problems: A double phase transition. Artificial Intelligence, 69(1–2):359–377, 1994.zbMATHCrossRefGoogle Scholar
  24. 24.
    R. Hojati, S. C. Krishnan, and R. K. Brayton. Early quantification and partitioned transition relations. In Proc. 1996 Int’l Conf. on Computer Design, pages 12–19, 1996.Google Scholar
  25. 25.
    S. Jha, Y. Lu, M. Minea, and E. M. Clarke. Equivalence checking using abstract BDDs. In Proc. Int’l Conf. on Computer Design (ICCD’97), pages 332–337, 1997.Google Scholar
  26. 26.
    T. Larrabee and Y. Tsuji. Evidence for a satisfiability threshold for random 3CNF formulas. In Working Notes of AAAI 1993 Spring Symposium: AI and NP-Hard Problems, pages 112–118, 1993.Google Scholar
  27. 27.
    J. P. Marques Silva and K. A. Sakallah. GRASP-A search algorithm for propositional satis-fiability. IEEE Trans. on Computers, 48(5):506–521, 1999.CrossRefGoogle Scholar
  28. 28.
    D. G. Mitchell and H. J. Levesque. Some pitfalls for experimenters with random SAT. Artificial Intelligence, 81(1–2):111–125, 1996.CrossRefMathSciNetGoogle Scholar
  29. 29.
    R. K. Ranjan, A. A. Aziz, R. K. Brayton, B. Plessier, and C. Pixley. Efficient formal design verification: Data structure + algorithms. Technical report, University of California at Berkeley, 1994. Tech. Rep. UCB/ERL M94/100.Google Scholar
  30. 30.
    B. Selman and S. Kirkpatrick. Critical behavior in the computational cost of satisfiability testing. Artificial Intelligence, 81(1–2):273–295, 1996.CrossRefMathSciNetGoogle Scholar
  31. 31.
    B. Selman, D. G. Mitchell, and H. J. Levesque. Generating hard satisfiability problems. Artificial Intelligence, 81(1–2):17–29, 1996.CrossRefMathSciNetGoogle Scholar
  32. 32.
    F. Somenzi. CUDD: CU Decision Diagram package. release 2.3.0., 1998. Dept. of Electrical and Computer Engineering. University of Colorado at Boulder.Google Scholar
  33. 33.
    R. E. Tarjan and M. Yannakakis. Simple linear-time algorithms to tests chordiality of graphs, tests acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs. SIAM J. on Computing, 13(3):566–579, 1984.zbMATHCrossRefMathSciNetGoogle Scholar
  34. 34.
    The VIS Group. VIS: A system for verification and synthesis. In Proc. 8th Int’l Conf. on Computer Aided Verification (CAV’ 96), pages 428–432, 1996. LNCS 1102. Ed. by R. Alur and T. Henziger.Google Scholar
  35. 35.
    T. E. Uribe and M. E. Stickel. Ordered binary decision diagrams and the Davis-Putnam procedure. In First Int’l Conf. on Constraints in Computational Logics, volume 845 of Lecture Notes in Computer Science, pages 34–49, Munich, September 1994. Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Alfonso San Miguel Aguirre
    • 1
  • MosheY. Vardi
    • 2
  1. 1.Dept. of Computer ScienceInstituto Tecnologico Autonomo de MexicoMexico CityMexico
  2. 2.Department of Computer ScienceRice UniversityHoustonUSA

Personalised recommendations