Lookahead in Partitioning SMT

TitleLookahead in Partitioning SMT
Publication TypeConference Paper
Year of Publication2021
AuthorsHyvärinen, Antti E. J., Marescotti Matteo, and Sharygina Natasha
Conference NameFormal Methods in Computer-Aided Design - FMCAD 2021
PublisherIEEE digital library
Conference LocationOnline Conference
Abstract

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.

Full Text