Combining SAT solvers on discrete resources

Abstract : We are interested in this work in solving efficiently a set of instances of the SAT problem using several solvers such as to minimize the total execution time. We propose two new approaches based on the usage of a representative benchmark of SAT instances. In the first approach, we improve a problem introduced in [7, 4] such as to reduce the number of unsolved SAT instances. The second approach extends a naive solution for combining SAT solvers in a parallel context in introducing the selection of a convenient set of SAT solvers. We study the theoretical properties of our approaches and realize many experiments using a benchmark of SAT instances. The obtained results show that it is interesting to combine SAT solvers for reducing the number of unsolved SAT instances and the mean execution time required to solve a set of SAT instances.
Type de document :
Communication dans un congrès
IEEE. HPCS '09 : International Conference on High Performance Computing & Simulation, Jun 2009, Leipzig, Germany. IEEE, pp.153-160, 2009, 〈10.1109/HPCSIM.2009.5194889〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00690807
Contributeur : Ist Rennes <>
Soumis le : mardi 24 avril 2012 - 14:43:03
Dernière modification le : mercredi 11 avril 2018 - 01:54:55

Identifiants

Collections

Citation

Yanik Ngoko, Denis Trystram. Combining SAT solvers on discrete resources. IEEE. HPCS '09 : International Conference on High Performance Computing & Simulation, Jun 2009, Leipzig, Germany. IEEE, pp.153-160, 2009, 〈10.1109/HPCSIM.2009.5194889〉. 〈hal-00690807〉

Partager

Métriques

Consultations de la notice

296