A DPLL(T) theory solver for quantified formulas

FORSYTE/RiSE hosting a talk by Tanja Schindler

DATE:	Monday, September 16, 2019
TIME:	11:00 c.t.
VENUE:	FAV Hörsaal 1 (ground floor), Favoritenstrasse 9-11, 1040, Vienna

ABSTRACT

First-order logic with quantifiers is undecidable in general, but some expressive fragments have complete instantiation. This means, it is sufficient to instantiate the quantified formulas with a finite set of ground terms computed from the formula, and then solve the resulting quantifier-free conjunction with an SMT solver. A challenge is to select the relevant instances in order to avoid producing too many new formulas that slow down the solver.

In this talk we will present a new approach that treats quantified formulas in SMT solvers in the style of a theory solver in the DPLL(T) framework. This comprises methods to detect instances of quantified formulas that are in conflict with the current boolean assignment of the ground literals or lead to a ground propagation. In particular, we will discuss how  E-matching, the most common heuristic method for quantifier instantiation in SMT solvers, can be used to find these specific instances. The presented approach is work in progress. Future work encompasses combining the approach with model-based quantifier instantiation in order to get completeness for decidable fragments.