Computing prime implicant

Abstract : Model checking and counter-example guided abstraction refinement are examples of applications of SAT solving requiring the production of models for satisfiable formulas. Better than giving a truth value to every variable, one can provide an implicant, i.e. a partial assignment of the variables such that every full extension is a model for the formula. An implicant is prime if every assignment is necessary. Since prime implicants contain no literal irrelevant for the satisfiability of the formula, they are considered as highly refined information. We here propose a novel algorithm that uses data structures found in modern CDCL SAT solvers to efficiently compute prime implicants starting from an existing model. The original aspects are (1) the algorithm is based on watched literals and a form of propagation of required literals, adapted to CDCL solvers (2) the algorithm works not only on clauses, but also on generalized constraints (3) for clauses and, more generally for cardinality constraints, the algorithm complexity is linear in the size of the constraints found. We implemented and evaluated the algorithm with the Sat4j library.
Type de document :
Communication dans un congrès
FMCAD - Formal Methods in Computer-Aided Design 2013, Oct 2013, Portland, United States. IEEE, pp.46-52, 2013, 〈http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/proceedings/54418_IEEE%20FMCAD_Complete%20Book.pdf〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00910363
Contributeur : Pascal Fontaine <>
Soumis le : mercredi 27 novembre 2013 - 20:47:29
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13

Identifiants

  • HAL Id : hal-00910363, version 1

Collections

Citation

David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure. Computing prime implicant. FMCAD - Formal Methods in Computer-Aided Design 2013, Oct 2013, Portland, United States. IEEE, pp.46-52, 2013, 〈http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/proceedings/54418_IEEE%20FMCAD_Complete%20Book.pdf〉. 〈hal-00910363〉

Partager

Métriques

Consultations de la notice

317