Hyvärinen, A., Marescotti, M., & Sharygina, N. (2021). Lookahead in Partitioning SMT. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 271–279). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_37
Lookahead in propositional satisfiability has proven
efficient as a heuristic in pre- and in-processing, for partitioning
instances for parallel solving, and as the main driver of a standalone
solver. While applying similar techniques in satisfiability
modulo theories is potentially equally useful, adapting lookahead
to learning theory clauses and to estimating search space sizes
in the presence of first-order structures is not straightforward.
This paper addresses both of these observations. We give a
hybrid algorithm that integrates lookahead into the state-based
representation of an SMT solver and show that in the vast
majority of cases it is possible to compute full lookahead up
to depth four on inexpensive theories. We also show the role of
first-order structures in SMT search space: while in most of our
benchmarks the partitions are easier to solve than the original
instance, we identify cases where lookahead results in sequences
of increasingly difficult instances for a computationally expensive
theory.
CC BY 4.0
