Sciweavers

IJCAI
1997

Hidden Gold in Random Generation of SAT Satisfiable Instances

13 years 5 months ago
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.
Thierry Castell, Michel Cayrol
Added 01 Nov 2010
Updated 01 Nov 2010
Type Conference
Year 1997
Where IJCAI
Authors Thierry Castell, Michel Cayrol
Comments (0)