Random 3-SAT: The Plot Thickens

Abstract. This paper presents an experimental investigation of the following questions: how does the averagecase 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 in the order? Is the transition dependent or independent of the solver? Our experiment design uses three complete SAT solvers embodying different 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 solverdependent. GRASP shifts from polynomial to exponential complexity near the density of 3.8, CPLEX shifts near density 3, while CUDD exhibits this transition between densities of 0.1 and 0.5. This experimental result underscores the dependence ...

• Type: Conference
• Year: 2000
• Where: CP
• Authors: Cristian Coarfa, Demetrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika Subramanian, Moshe Y. Vardi
• Keywords: Artificial Intelligence, Complexity Phase Transition, Complexity Shifts, CP 2000, Phase Transition