Hidden Gold in Random Generation of SAT Satisfiable Instances
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence. Constraint Satisfaction. Pages 372-376.
Abstract
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-~utnam" procedure (which is complete), and the two mcomplete methods: GSA T and the Break Out Method. Moreover, a new method for escaping from local minima is presented.
@inproceedings{ijcai1997p55,
title = {Hidden Gold in Random Generation of SAT Satisfiable Instances},
author = {Castell, Thierry and Cayrol, Michel},
booktitle = {Proceedings of the Fifteenth International Joint Conference on
Artificial Intelligence, {IJCAI-97}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Martha E. Pollack},
pages = {372--376},
year = {1997},
note = {Constraint Satisfaction},
url = {https://ijcai.org/proceedings/1997/55},
}
TY - CPAPER TI - Hidden Gold in Random Generation of SAT Satisfiable Instances AU - Castell, Thierry AU - Cayrol, Michel T2 - Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI-97 PB - International Joint Conferences on Artificial Intelligence PY - 1997 SP - 372 EP - 376 UR - https://ijcai.org/proceedings/1997/55 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
