Evaluation of incomplete algorithms that solve SAT requires to generate hard satisfiable instances. For that purpose, the kSAT unifomr 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.
展开▼
