A verified SAT solver with watched literals using imperative HOL

Abstract : Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isa-belle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.
Type de document :
Communication dans un congrès
CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. ACM Press, 2018, 〈10.1145/3167080〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01904647
Contributeur : Jasmin Christian Blanchette <>
Soumis le : jeudi 25 octobre 2018 - 11:05:40
Dernière modification le : mercredi 7 novembre 2018 - 15:13:31

Fichier

sat_2wl_paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich. A verified SAT solver with watched literals using imperative HOL. CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. ACM Press, 2018, 〈10.1145/3167080〉. 〈hal-01904647〉

Partager

Métriques

Consultations de la notice

24

Téléchargements de fichiers

8