Abstract
This paper presents an elegant algorithm for existential quantifier elimination using incremental SAT solving. This approach contrasts with existing techniques in that it is based solely on manipulating the SAT instance rather than requiring any reengineering of the SAT solver or needing an auxiliary data-structure such as a BDD. The algorithm combines model enumeration with the generation of shortest prime implicants so as to converge onto a quantifier-free formula presented in CNF. We apply the technique to a number of hardware circuits and transfer functions to demonstrate the effectiveness of the method.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aloul, F.A., Markov, I.L., Sakallah, K.A.: Faster SAT and Smaller BDDs via Common Function Structure. In: ICCAD, pp. 443–448 (2001)
Armstrong, T., Marriott, K., Schachte, P., Søndergaard, H.: Two Classes of Boolean Functions for Dependency Analysis. Sci. Comp. Program. 31(1), 3–45 (1998)
Barrett, E., King, A.: Range and Set Abstraction Using SAT. Electronic Notes in Theoretical Computer Science 267(1), 17–27 (2010)
Blake, A.: Canonical expressions in Boolean algebra. University of Chicago, Chicago (1938)
Brauer, J., King, A.: Automatic abstraction for intervals using boolean formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 167–183. Springer, Heidelberg (2010)
Brauer, J., King, A.: Approximate quantifier elimination for propositional boolean formulae. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 73–88. Springer, Heidelberg (2011)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The mathSAT 4 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)
Bryant, R.: Boolean analysis of MOS circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 6(4), 634–649 (1987)
Bryant, R.E.: A view from the engine room: Computational support for symbolic model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 145–149. Springer, Heidelberg (2008), http://www.slidefinder.net/m/mc25/7464626
Burch, J.R., Clarke, E.M., McMillan, K.L.: Symbolic model checking: 1020 states and beyond. Information and Computation 98, 142–170 (1992)
Cavada, R., Cimatti, A., Franzén, A., Kalyanasundaram, K., Roveri, M., Shyamasundar, R.K.: Computing predicate abstractions by integrating BDDs and SMT solvers. In: FMCAD, pp. 69–76. IEEE Computer Society Press, Los Alamitos (2007)
Chauhan, P., Clarke, E.M., Kroening, D.: A SAT-based algorithm for reparameterization in symbolic simulation. In: DAC, pp. 524–529. ACM Press, New York (2004)
Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 78–92. Springer, Heidelberg (2004)
Cook, B., Kroening, D., Rümmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 236–250. Springer, Heidelberg (2010)
Coudert, O., Madre, J.C.: Implicit and Incremental Computation of Primes and Essential Primes of Boolean Functions. In: DAC, pp. 36–39. IEEE Computer Society Press, Los Alamitos (1992)
Damiano, R.F., Kukula, J.H.: Checking satisfiability of a conjunction of BDDs. In: DAC, pp. 818–823. ACM Press, New York (2003)
Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)
Eén, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT. JSAT 2(1-4), 1–26 (2006)
Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: POPL, pp. 191–202. ACM Press, New York (2002)
Genaim, S., Giacobazzi, R., Mastroeni, I.: Modeling Secure Information Flow with Boolean Functions. In: IFIP WG 1.7, ACM Workshop on Issues in the Theory of Security, Barcelona, Spain, pp. 55–66 (2004)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Gupta, A., Yang, Z.-J., Ashar, P., Gupta, A.: SAT-based image computation with application in reachability analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 354–371. Springer, Heidelberg (2000)
Jin, H., Somenzi, F.: CirCUs: A hybrid satisfiability solver. In: Holger Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 211–223. Springer, Heidelberg (2005)
Kettle, N., King, A., Strzemecki, T.: Widening rOBDDs with prime implicants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 105–119. Springer, Heidelberg (2006)
Knuth, D.E.: The Art of Computer Programming, vol. 3. Addison-Wesley, London (1997)
Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 141–153. Springer, Heidelberg (2003)
Lahiri, S.K., Nieuwenhuis, R., Oliveras, A.: SMT techniques for fast predicate abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 424–437. Springer, Heidelberg (2006)
Manquinho, V.M., Flores, P.F., Silva, J.P.M., Oliveira, A.L.: Prime Implicant Computation Using Satisfiability Algorithms. In: International Conference on Tools with Artificial Intelligence, pp. 232–239. IEEE Computer Society Press, Los Alamitos (1997)
McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002)
Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 585–599. Springer, Heidelberg (2010)
Plaisted, D., Greenbaum, S.: A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation 2(3), 293–304 (1986)
Quine, W.V.: A way to simplify truth functions. American Mathematical Monthly 62(9), 627–631 (1955)
Read, R.C.: Everyone a Winner. Annals of Discrete Mathematics 2, 107–120 (1978)
Saïdi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 443–454. Springer, Heidelberg (1999)
Samson, E.W., Mills, B.E.: Circuit minimization: Algebra and algorithms for new Boolean canonical expressions. Technical Report TR, pp. 21–54. United States Air Force, Cambridge Research Lab (1954)
Schlich, B.: Model checking of software for microcontrollers. ACM Trans. Embedded Comput. Syst 9(4), article Number 36 (2010)
Sheng, S., Hsiao, M.S.: Efficient Preimage Computation Using A Novel Success-Driven ATPG. In: DATE, pp. 10822–10827. IEEE Computer Society Press, Los Alamitos (2003)
Umans, C.: The Minimum Equivalent DNF Problem and Shortest Implicants. In: FOCS, pp. 556–563. IEEE Computer Society Press, Los Alamitos (1998)
Weaver, S., Franco, J.V., Schlipf, J.S.: Extending Existential Quantification in Conjunctions of BDDs. JSAT 1(2), 89–110 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brauer, J., King, A., Kriener, J. (2011). Existential Quantification as Incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds) Computer Aided Verification. CAV 2011. Lecture Notes in Computer Science, vol 6806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22110-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-22110-1_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22109-5
Online ISBN: 978-3-642-22110-1
eBook Packages: Computer ScienceComputer Science (R0)