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

• Type: Conference
• Year: 2001
• Where: CP
• Authors: Alfonso San Miguel Aguirre, Moshe Y. Vardi
• Keywords: Artificial Intelligence, CP 2001, Crossover Density, Median Running Times, Running Time