2023/03/27 by Eugene P. Goldberg, Goldberg, Eugene
Computer Science · #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Parallel Computing and Optimization Techniques
paper · pdf · doi:10.48550/arxiv.2303.14928
openalex publication_date 2023/03/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 partial QE (or PQE for short). PQE allows to unquantify a part 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 VerPQE and provide some experimental results.