Lookahead in Partitioning SMT

Formal Methods in Computer-Aided Design (FMCAD)


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.

Related Publications

All Publications

PETS - July 16, 2021

HashWires: Hyperefficient Credential-Based Range Proofs

Konstantinos (Kostas) Chalkias, Shir Cohen, Kevin Lewi, Fredric Moezinia, Yolan Romailler

ICML - July 19, 2021

Making Paper Reviewing Robust to Bid Manipulation Attacks

Ruihan Wu, Chuan Guo, Felix Wu, Rahul Kidambi, Laurens van der Maaten, Kilian Q. Weinberger

IEEE Access Journal (IEEE Access) - August 1, 2021

Coded Machine Unlearning

Nasser Aldaghri, Hessam Mahdavifar, Ahmad Beirami

PLDI - June 16, 2021

Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption

Meghan Cowan, Deeksha Dangwal, Armin Alaghi, Caroline Trippel, Vincent T. Lee, Brandon Reagen

To help personalize content, tailor and measure ads, and provide a safer experience, we use cookies. By clicking or navigating the site, you agree to allow our collection of information on and off Facebook through cookies. Learn more, including about available controls: Cookies Policy