Circuit Based Encoding of CNF formula

Abstract. 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 con-junction 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 formula is satisfiable, our proposed translation delivers a full circuit formula. A new incremental preprocessing process is designed leading to interesting experimental improvements of Minisat a state-of-the-art satisfiability solver. Finally, using our circuit encoding, on many SAT instances interesting results are also obtained wrt. the backdoor set computation problem.