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.
Document type :
Conference papers
Liste complète des métadonnées
Contributor : Pascal Fontaine <>
Submitted on : Wednesday, November 27, 2013 - 8:47:29 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM


  • HAL Id : hal-00910363, version 1


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. pp.46-52. ⟨hal-00910363⟩



Record views