Verification Of Partial Quantifier Elimination
share
Quantifier elimination (QE) is an important problem that has numerous applications. Unfortunately, QE is computationally very hard. Earlier we introduced a generalization of QE called 𝑝𝑎𝑟𝑡𝑖𝑎𝑙 QE (or PQE for short). PQE allows to unquantify a 𝑝𝑎𝑟𝑡 of the formula. The appeal of PQE is twofold. First, many important problems can be solved in terms of PQE. Second, PQE can be drastically faster than QE if only a small part of the formula gets unquantified. To make PQE practical, one needs an algorithm for verifying the solution produced by a PQE solver. In this paper, we describe a very simple SAT-based verifier called 𝑉𝑒𝑟𝑃𝑄𝐸 and provide some experimental results.
READ FULL TEXT