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. 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 the Minisat satisfiability solver.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Audemard, G., Sais, L.: Circuit Based Encoding of CNF formulas. Technical report, CRIL (2007)
Boufkhad, Y.: Aspects probabilistes et algorithmiques du problème de satisfiabilité. Phd thesis, Université de Paris 6, Laboratoire d’ Informatique de Paris 6 (1996)
Dubois, O., Boufkhad, Y.: A general upper bound for the satisfiability threshold of random r-SAT formulae. Journal of Algorithms 24(2), 395–420 (1997)
Gallo, G., Urbani, G.: Algorithms for testing the satisfiability of propositional formulae. Journal of logic programming 7(1), 45–61 (1989)
Giunchiglia, E., Maratea, M., Tacchella, A.: Dependent and independent variables in propositional satisfiability. In: Flesca, S., et al. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 296–307. Springer, Heidelberg (2002)
Gregoire, E., et al.: Automatic extraction of functional dependencies. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 122–132. Springer, Heidelberg (2005)
Lu, F., et al.: A circuit sat solver with signal correlation guided learning. In: Proceedings of international conference DATE, pp. 892–897 (2003)
Purdom, P.W.: Solving satisfiability with less searching. IEEE transactions on pattern analysis and machine intelligence 6(4), 510–513 (1984)
Roy, J., Markov, I., Bertacco, V.: Restoring circuit structure from SAT instances. In: Proceedings of international workshop on Logic and synthesis (2004)
Selman, B., Kautz, H., McAllester, D.: Ten challenges in propositional reasoning and search. In: Proceedings of IJCAI (1997)
Walsh, T., Bacchus, F., Thiffault, C.: Solving Non-clausal Formulas with DPLL Search. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 663–678. Springer, Heidelberg (2004)
Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proceedings of IJCAI, pp. 1173–1178 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Audemard, G., Saïs, L. (2007). Circuit Based Encoding of CNF Formula. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72787-3
Online ISBN: 978-3-540-72788-0
eBook Packages: Computer ScienceComputer Science (R0)