Relevancy propagation for efficient theory combination

摘要

Relevancy propagation for efficient theory combination is described. In one implementation, an efficient SMT solver dynamically applies relevancy propagation to limit propagation of unnecessary constraints in a DPLL-based solver. This provides a drastic increase in speed and performance over conventional DPLL-based solvers. The relevancy propagation is guided by relevancy rules, which in one implementation emulate Tableau rules for limiting constraint propagation, while maintaining the performance of efficient DPLL-based solvers. An exemplary solver propagates truth assignments to constraints of a formula, and tracks which truth assignments are relevant for determining satisfiability of the formula. The solver propagates truth assignments that were marked relevant to a theory solver, while avoiding propagation of irrelevant truth assignments. The efficient SMT solver provides a drastic reduction in search space covered during quantifier instantiation and offers profound acceleration during bit-vectors reasoning.