Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis

Most state-of-the-art approaches for Satisfiability Modulo Theories (SMT(T)) rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory T (T-solver). Often T is the combination T-1 boolean OR T-2 of two (or more) simpler theories (SMT(T-1 boolean OR T-2)), s.t. the specific T-i-solvers must be combined. Up to a few years ago, the standard approach to SMT(T-1 boolean OR T-2) was to integrate the SAT solver with one combined T-1 boolean OR T-2-solver, obtained from two distinct T-i-solvers by means of evolutions of Nelson and Oppen's (NO) combination procedure, in which the T-i-solvers deduce and exchange interface equalities. Nowadays many state-of-the-art SMT solvers use evolutions of a more recent SMT(T-1 boolean OR T-2) procedure called Delayed Theory Combination (DTC), in which each T-i-solver interacts directly and only with the SAT solver, in such a way that part or all of the (possibly very expensive) reasoning effort on interface equalities is delegated to the SAT solver itself. In this paper we present a comparative analysis of DTC vs. NO for SMT(T-1 boolean OR T-2). On the one hand, we explain the advantages of DTC in exploiting the power of modern SAT solvers to reduce the search. On the other hand, we show that the extra amount of Boolean search required to the SAT solver can be controlled. In fact, we prove two novel theoretical results, for both convex and non-convex theories and for different deduction capabilities of the T-i-solvers, which relate the amount of extra Boolean search required to the SAT solver by DTC with the number of deductions and case-splits required to the T-i-solvers by NO in order to perform the same tasks: (i) under the same hypotheses of deduction capabilities of the T-i-solvers required by NO, DTC causes no extra Boolean search; (ii) using T-i-solvers with limited or no deduction capabilities, the extra Boolean search required can be reduced down to a negligible amount by controlling the quality of the T-conflict sets returned by the T-solvers.