Juan A. Navarro, Andrei Voronkov
We present the results from experiments with a new family of random formulas for the satisfiability problem. Our proposal is a generalisation of the random k-SAT model that introduces non-clausal formulas and exhibits interesting features such as experimentally observed sharp phase transition and the easy-hard-easy pattern. The experimental results provide some insights on how the use of different clausal translations can affect the performance of satisfiability solving algorithms. We also expect our model to provide diverse and challenging benchmarks for developers of SAT procedures for non-clausal formulas.
Content Area: 6. Constraint Satisfaction and Satisfiability
Subjects: 15.2 Constraint Satisfaction
Submitted: May 10, 2005