Circuit Based Encoding of CNF Formula

In this paper a new circuit sat based encoding of boolean formula is proposed. It makes an original use of the concept of restrictive models introduced by Boufkhad to polynomially translate any formula in conjunctive normal form (CNF) to a circuit sat representation (a conjunction of gates and clauses). Our proposed encoding preserves the satisfiability of the original formula. The set of models of the obtained circuit w.r.t. the original set of variables is a subset of the models (with special characteristics) of the original formula. Each gate represents both a subset of clauses from the original CNF formula and a set of new additional clauses which constrains the set of models to those with a special structure. Using two variant of restrictive models, our circuit sat based encoding leads to a conjunction of two sub-formulas: a set of gates and a horn formula. We also provided a connection between our encoding and the satisfiability of the original formula i.e. when the input formu...

• Type: Conference
• Year: 2007
• Where: SAT
• Authors: Gilles Audemard, Lakhdar Sais
• Keywords: Circuit Sat Representation, Original Formula, Restrictive Models, SAT 2007