Shared-Context Batched Satisfiability
For program analyzer designers, this work provides a formalization and algorithmic options for efficiently handling batches of related SMT queries, though the contribution is incremental as it combines existing ideas with a new algorithm.
The paper formalizes Shared-Context Batched Satisfiability, where multiple SMT queries share a context, and evaluates three strategies: predicate-by-predicate, disjunctive over-approximation, and a new algorithm CLF. Results show no single strategy dominates; over-approximation is fastest on solved symbolic-abstraction queries, while CLF solves more hard instances and is fastest on active property checking.
Program analyzers often issue batches of SMT queries that share a large symbolic context and differ only in a small predicate. We formalize this recurring pattern as \emph{Shared-Context Batched Satisfiability}: given a formula $φ$ and predicates $P$, determine whether $φ\land p$ is satisfiable for each $p \in P$. We study three theory-agnostic strategies for this problem: predicate-by-predicate checking, disjunctive over-approximation, and Core-Literal Filter (CLF), a new algorithm that learns literals inconsistent with $φ$ and uses them to reject later predicates. Our evaluation on symbolic abstraction and active property checking shows that no strategy dominates universally: over-approximation is fastest on solved symbolic-abstraction queries, while CLF increases the number of solved hard instances and is fastest on active property checking. We advocate treating shared-context batched satisfiability as a first-class primitive in design program analyzers and exploring the algorithmic design space more systematically.