Hidden Gold in Random Generation of SAT Satisfiable Instances

Evaluation of incomplete algorithms that solve SAT requires to generate hard satisfiable instances. For that purpose, the kSAT uniform random generation is not usable. The other generators of satisfiable instances generate instances that are not intrinsically hard, or exhaustive tests have not been done for determining hard and easy areas. A simple method for generating random hard satisfiable instances is presented. Instances are empirically shown to be hard for three classical methods: the "Davis-Putnam" procedure (which is complete), and the two incomplete methods: GSAT and the Break Out Method. Moreover, a new method for escaping from local minima is presented.

• Type: Conference
• Year: 1997
• Where: IJCAI
• Authors: Thierry Castell, Michel Cayrol
• Keywords: Hard Satisfiable Instances, IJCAI 1997, IJCAI 2007, Satisfiable Instances, Uniform Random Generation