×

zbMATH — the first resource for mathematics

Random 3-SAT and BDDs: The plot thickens further. (English) Zbl 1067.68668
Walsh, Toby (ed.), Principles and practice of constraint programming - CP 2001. 7th international conference, Paphos, Cyprus, November 26 – December 1, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42863-1). Lect. Notes Comput. Sci. 2239, 121-136 (2001).
Summary: 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.
For the entire collection see [Zbl 0984.00059].

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q25 Analysis of algorithms and problem complexity
Software:
CUDD
PDF BibTeX XML Cite
Full Text: Link