# Random 3-SAT and BDDs: The Plot Thickens Further

## 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## Preview

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.J. Balcazar. Self-reducibility.
*Journal of Computer and System Sciences*, 41(3):367–388, 1990.zbMATHCrossRefMathSciNetGoogle Scholar - 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.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.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.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.R. E. Bryant. Graph-based algorithms for Boolean function manipulation.
*IEEE Trans. on Computers*, 35(8):677–691, 1986.zbMATHCrossRefGoogle Scholar - 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.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.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.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.V. Chvátal and E. Szemerédi. Many hard examples for resolution.
*J. of the ACM*, 35(4):759–768, 1988.zbMATHCrossRefGoogle Scholar - 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.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.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.M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving.
*Comm. of the ACM*, 5:394–397, 1962.zbMATHCrossRefMathSciNetGoogle Scholar - 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.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.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.I. P. Gent and T. Walsh. Easy problems are sometimes hard.
*Artificial Intelligence*, 70(1–2):335–345, 1994.zbMATHCrossRefMathSciNetGoogle Scholar - 21.J. F. Groote. Hiding propositional constants in BDDs.
*Formal Methods in System Design*, 8:91–96, 1996.CrossRefGoogle Scholar - 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.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.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.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.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.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.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.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.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.B. Selman, D. G. Mitchell, and H. J. Levesque. Generating hard satisfiability problems.
*Artificial Intelligence*, 81(1–2):17–29, 1996.CrossRefMathSciNetGoogle Scholar - 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.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.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.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