Complete Trigger Selection in Satisfiability modulo first-order Theories

TL;DR

This paper demonstrates that an SMT solver's completeness and decision capabilities can be achieved by aligning its trigger function with the literal selection function, especially for specific clause classes like Horn or 2SAT.

Contribution

It establishes a complete trigger selection method for SMT solvers based on resolution saturation and literal selection, enabling polynomial-time solving for certain clause classes.

Findings

T is complete if its Trigger function matches the literal selection function.

T halts with a ground model G, which can be extended to a model in S.

T solves Horn or 2SAT clauses in polynomial time.

Abstract

Let T be an SMT solver with no theory solvers except for Quantifier Instantiation. Given a set of first-order clauses S saturated by Resolution (with a valid literal selection function) we show that T is complete if its Trigger function is the same as the literal selection function. So if T halts with a ground model G, then G can be extended to a model in the theory of S. In addition for a suitable ordering, if all maximal literals are selected in each clause, then T will halt on G, so it is a decision procedure for the theory S. Also, for a suitable ordering, if all clauses are Horn, or all clauses are 2SAT, then T solves the theory S in polynomial time.