SMT solvers that perform search over a large set of constraints need to maintain, update and propagate truth assignments to atomic constraints. Each new truth assignment may lead to additional constraint propagation, which depending on the constraint domain can be costly. Relevancy propagation keeps track of which truth assignments are essential for determining satisfiability of a formula. Atoms that are marked as relevant have their truth assignment propagated to theory solvers, but we can avoid propagating truth assignments for atoms that are not marked as relevant.

PDF file

Details