Partial Quantifier Elimination
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.
Unable to display preview. Download preview PDF.
- 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.Goldberg, E., Manolios, P.: Quantifier elimination by dependency sequents. In: FMCAD 2012, pp. 34–44 (2012)Google Scholar
- 7.Goldberg, E., Manolios, P.: Quantifier elimination via clause redundancy. In: FMCAD 2013, pp. 85–92 (2013)Google Scholar
- 8.Goldberg, E., Manolios, P.: Bug hunting by computing range reduction. Technical Report arXiv:1408.7039 [cs.LO] (2014)Google Scholar
- 9.Goldberg, E., Manolios, P.: Partial quantifier elimination. Technical Report arXiv:1407.4835 [cs.LO] (2014)Google Scholar
- 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
- 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.HWMCC-2010 benchmarks, http://fmv.jku.at/hwmcc10/benchmarks.html