Partial Quantifier Elimination

  • Eugene Goldberg
  • Panagiotis Manolios
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8855)

Abstract

We consider the problem of Partial Quantifier Elimination (PQE). Given formula ∃ X[F(X,Y) ∧ G(X,Y)], where F, G are in conjunctive normal form, the PQE problem is to find a formula F *(Y) such that F * ∧ ∃ X[G] ≡ ∃ X[F ∧ G]. We solve the PQE problem by generating and adding to F clauses over the free variables that make the clauses of F with quantified variables redundant in ∃ X[F ∧ G]. The traditional Quantifier Elimination problem (QE) can be viewed as a degenerate case of PQE where G is empty so all clauses of the input formula with quantified variables need to be made redundant. The importance of PQE is threefold. First, in non-degenerate cases, PQE can be solved more efficiently than QE. Second, many problems are more naturally formulated in terms of PQE rather than QE. Third, an efficient PQE-algorithm will enable new methods of model checking and SAT-solving. We describe a PQE algorithm based on the machinery of dependency sequents and give experimental results showing the promise of PQE.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 101–115. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)CrossRefGoogle Scholar
  3. 3.
    Chauhan, P., Clarke, E., Jha, S., Kukula, J., Veith, H., Wang, D.: Using combinatorial optimization methods for quantification scheduling. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 293–309. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Goldberg, E., Manolios, P.: SAT-solving based on boundary point elimination. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC 2010. LNCS, vol. 6504, pp. 93–111. Springer, Heidelberg (2010)Google Scholar
  6. 6.
    Goldberg, E., Manolios, P.: Quantifier elimination by dependency sequents. In: FMCAD 2012, pp. 34–44 (2012)Google Scholar
  7. 7.
    Goldberg, E., Manolios, P.: Quantifier elimination via clause redundancy. In: FMCAD 2013, pp. 85–92 (2013)Google Scholar
  8. 8.
    Goldberg, E., Manolios, P.: Bug hunting by computing range reduction. Technical Report arXiv:1408.7039 [cs.LO] (2014)Google Scholar
  9. 9.
    Goldberg, E., Manolios, P.: Partial quantifier elimination. Technical Report arXiv:1407.4835 [cs.LO] (2014)Google Scholar
  10. 10.
    Goldberg, E., Manolios, P.: Software for quantifier elimination in propositional logic. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 291–294. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  11. 11.
    Jin, H., Somenzi, F.: Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In: DAC 2005, pp. 750–753 (2005)Google Scholar
  12. 12.
    Brauer, J., King, A., Kriener, J.: Existential quantification as incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 191–207. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  13. 13.
    Jiang, J.-H.R.: Quantifier elimination via functional composition. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 383–397. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Klieber, W., Janota, M., Marques-Silva, J., Clarke, E.: Solving QBF with free variables. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 415–431. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  15. 15.
    Kullmann, O.: New methods for 3-sat decision and worst-case analysis. Theor. Comput. Sci. 223(1-2), 1–72 (1999)CrossRefMATHMathSciNetGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Ganai, M.K., Gupta, A., Ashar, P.: Efficient sat-based unbounded symbolic model checking using circuit cofactoring. In: ICCAD 2004, pp. 510–517 (2004)Google Scholar
  18. 18.

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Eugene Goldberg
    • 1
  • Panagiotis Manolios
    • 1
  1. 1.Northeastern UniversityUSA

Personalised recommendations