Project: Propositional satisfiability
Contact: Moshe Y. Vardi
Devika Subramanian
Demetrios Demopoulos
WWW page: not available
Description: We investigate emprirically questions regarding the satisfiability (SAT) problem like the following:
  • how does the average-case complexity of random 3-SAT depend on the density?
  • is there a phase transition in which the complexity shifts from polynomial to exponential?
  • is the transition dependent or independent of the solver?
These questions are studied by gathering running times for a large collection of random 3-SAT problems using different SAT solvers embodying very different underlying algorithms: GRASP, CPLEX and CUDD.