Skip to main content
SpringerLink
Log in
Book cover

International Conference on Principles and Practice of Constraint Programming

CP 2000: Principles and Practice of Constraint Programming – CP 2000 pp 143–159Cite as

Random 3-SAT: The Plot Thickens

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1894))

Abstract

This paper presents an experimental investigation of the following questions: how does the average-case complexity of random 3-SAT, understood as a function of the order (number of variables) for fixed density (ratio of number of clauses to order) instances, depend on the density? Is there a phase transition in which the complexity shifts from polynomial to exponential? Is the transition dependent or independent of the solver? To study these questions, we gather median and mean running times for a large collection of random 3-SAT problems while systematically varying both densities and the order of the instances. We use three different complete SAT solvers, embodying very different underlying algorithms: GRASP, CPLEX, and CUDD. We observe new phase transitions for all three solvers, where the median running time shifts from polynomial in the order to exponential. The location of the phase transition appears to be solver-dependent. While GRASP and CUDD shift from polynomial to exponential complexity at a density of about 3.8, CUDD exhibits this transition between densities of 0.1 and 0.5. We believe these experimental observations are important for understanding the computational complexity of random 3-SAT, and can be used as a justification for developing density-aware solvers for 3-SAT.

Supported in part by NSF grant CCR-9700061, and by a grant from the Intel Corporation.

This work was done while the author was on sabbatical at Rice University, supported in part by CONACyT grant 145502.

Supported in part by NSF grant IRI-9796046.

Supported in part by NSF grant CCR-9700061, and by a grant from the Intel Corporation.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

  3. 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 

  4. R. E. Bixby. Implementing the Simplex method: The initial basis. ORSA J. on Computing, 4(3):267–284, 1992.

    MATH  MathSciNet  Google Scholar 

  5. 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 

  6. A. Z. Broder, A. M. Frieze, and E. Upfal. On the satisfiability and maximum satisfiability of random 3-CNF formulas. In Proc. 4th Annual ACM-SIAM Symp. on Discrete Algorithms, pages 322–330, 1993.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  8. M. Chao and J. V. Franco. Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiability problem. Information Sciences, 51:289–314, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  9. 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 

  10. V. Chvátal and E. Szemerédi. Many hard examples for resolution. J. of the ACM, 35(4):759–768, 1988.

    Article  MATH  Google Scholar 

  11. J. M. Crawford and L. D. Auton. Experimental results on the crossover point in satisfiability problems. AAAI, pages 21–27, 1993.

    Google Scholar 

  12. 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.

    Article  MathSciNet  Google Scholar 

  13. M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Comm. of the ACM, 5:394–397, 1962.

    Article  MATH  Google Scholar 

  14. O. Dubois, Y. Boufkhad, and J. Mandler. Typical random 3-SAT formulae and the satisfiability theshold. In Proc. 11th Annual ACM-SIAM Symp. on Discrete Algorithms, pages 126–127, 2000.

    Google Scholar 

  15. E. Friedgut. Necessary and sufficient conditions for sharp threshold of graph properties and the k-SAT problem. J. Amer. Math. Soc., 12:1917–1054, 1999.

    Article  MathSciNet  Google Scholar 

  16. A. Frieze and S. Suen. Analysis of two simple heuristics for random instances of k-SAT. J. of Algorithms, 20(2):312–355, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  17. I. P. Gent and T. Walsh. The SAT phase transition. In Proc. European Conf. on Artificial Intelligence, pages 105–109, 1994.

    Google Scholar 

  18. J. F. Groote. Hiding propositional constants in BDDs. Formal Methods in System Design, 8:91–96, 1996.

    Article  Google Scholar 

  19. 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 

  20. T. Hogg and C. P. Williams. The hardest constraint problems: A double phase transition. Artificial Intelligence, 69(1–2):359–377, 1994.

    Article  MATH  Google Scholar 

  21. J. N. Hooker. Resolution vs. cutting plane solution of inference problems: Some computational experience. Operations Research Letters, 7:1–7, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  22. S. Kirkpatrick and B. Selman. Critical behavior in the satisfiability of random formulas. Science, 264:1297–1301, 1994.

    Article  MathSciNet  Google Scholar 

  23. T. Larrabee and Y. Tsuji. Evidence for a satisfiability threshold for random 3CNF formulas. Technical report, University of California, Santa Cruz, 1992. Technical report USCS-CRL-92042.

    Google Scholar 

  24. J. P. Marques Silva and K. A. Sakallah. GRASP-A search algorithm for propositional satisfiability. IEEE Trans. on Computers, 48(5):506–521, 1999.

    Article  MathSciNet  Google Scholar 

  25. D. G. Mitchell and H. J. Levesque. Some pitfalls for experimenters with random SAT. Artificial Intelligence, 81(1–2):111–125, 1996.

    Article  MathSciNet  Google Scholar 

  26. M. Mitzenmacher. Tight thresholds for the pure literal rule. Technical report, Digital System Research Center, Palo Alto, California, 1997. SRC Technical Note 1997-011.

    Google Scholar 

  27. G. J. Nam, K. A. Sakallah, and R. A. Rutenbar. Satisfiability-based layout revisited: Detailed routing of complex fpgas via search-based boolean sat. In Proc. ACM Int’l Symp. on Field-Programmable Gate Arrays (FPGA’99), pages 167–175, 1999.

    Google Scholar 

  28. B. Selman and S. Kirkpatrick. Critical behavior in the computational cost of satisfiability testing. Artificial Intelligence, 81(1–2):273–295, 1996.

    Article  MathSciNet  Google Scholar 

  29. B. Selman, D. G. Mitchell, and H. J. Levesque. Generating hard satisfiability problems. Artificial Intelligence, 81(1–2):17–29, 1996.

    Article  MathSciNet  Google Scholar 

  30. B. M. Smith and M. E. Dyer. Locating the phase transition in binary constraint satisfaction problems. Artificial Intelligence Journal, 8(1–2):155–181, 1996.

    Article  MathSciNet  Google Scholar 

  31. 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 

  32. P. Svenson and M. G. Nordahl. Relaxation in graph coloring and satisfiability problems. Phys. Rev. E, 59(4):3983–3999, 1999.

    Article  Google Scholar 

  33. 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 

  34. 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.

    Chapter  Google Scholar 

Download references

Author information

Author notes

  1. Alfonso San Miguel Aguirre

    Present address: Dept. of Computer Science, Instituto Tecnologico Autonomo de Mexico, Rio Hondo 1, 01000, Mexico City

Authors and Affiliations

  1. Department of Computer Science, Rice University, 6100 S. Main St, MS 132, Houston, TX, 77005-1892

    Cristian Coarfa, Demetrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika Subramanian & Moshe Y. Vardi

Authors
  1. Cristian Coarfa
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Demetrios D. Demopoulos
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alfonso San Miguel Aguirre
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Devika Subramanian
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of California at Irvine, Irvine, CA, 92697, USA

    Rina Dechter

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coarfa, C., Demopoulos, D.D., Aguirre, A.S.M., Subramanian, D., Vardi, M.Y. (2000). Random 3-SAT: The Plot Thickens. In: Dechter, R. (eds) Principles and Practice of Constraint Programming – CP 2000. CP 2000. Lecture Notes in Computer Science, vol 1894. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45349-0_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-45349-0_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41053-9

  • Online ISBN: 978-3-540-45349-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation