Table-based Quantifier Elimination
This work offers a novel instantiation method for quantifier elimination in guarded formulas, but its impact is limited as it does not improve standard SMT benchmarks and only shows gains on SAT/ASP benchmarks.
The paper proposes a table-based quantifier elimination method for guarded formulas, implemented as a pre-processor for SMT solvers using SQLite. While it does not accelerate SMT-LIB 2025 benchmarks, it improves performance on SAT and ASP solver benchmarks, with applications in graph problems.
Quantifiers make first-order logic more expressive than propositional logic, but they also make solving satisfiability problems more difficult. To solve these problems efficiently, many techniques have been developed to eliminate quantifiers from logic formulas: model-based quantifier instantiation, E-matching, Skolemization, destructive equality resolution, ... I propose a table-based instantiation method for quantifier elimination. It can be used to solve satisfiability problems for "guarded" formulas, i.e., formulas where the use of defined functions in the matrix of quantifications effectively restricts the relevant range of their variables to a finite set. I have implemented this method in a pre-processor for SMT solvers. This "grounder" leverages an embedded relational database (SQLite) to execute relational operations efficiently. While this grounder does not accelerate 2025 benchmarks of the SMT-LIB library, it does improve performance of SMT solvers on public benchmarks for SAT and ASP solvers. The grounder has applications in, e.g., solving graph problems.