Sciweavers

Share
CP
2000
Springer

Random 3-SAT: The Plot Thickens

9 years 2 months ago
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 ...
Cristian Coarfa, Demetrios D. Demopoulos, Alfonso
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where CP
Authors Cristian Coarfa, Demetrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika Subramanian, Moshe Y. Vardi
Comments (0)
books