Lookahead-Based SMT Solving

Antti Hyyvarinen, Matteo Marescotti, Parvin Sadigova, Hana Chockler, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

1 Citation (Scopus)
117 Downloads (Pure)

Abstract

The lookahead approach for binary-tree-based search in constraint solving favors branching that provide the lowest upper bound for the remaining search space. The approach has recently been applied in instance partitioning in divide-and-conquer-based parallelization, but in general its connection to modern, clause-learning solvers is poorly understood. We show two ways of combining lookahead approach with a modern DPLL(T)-based SMT solver fully profiting from theory propagation, clause learning, and restarts. Our thoroughly tested prototype implementation is surprisingly efficient as an independent SMT solver on certain instances, in particular when applied to a non-convex theory, where the lookahead-based implementation solves 40% more unsatisfiable instances compared to the standard implementation.
Original languageEnglish
Title of host publicationLPAR-22
Subtitle of host publicationLPAR-22: 22ND INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING
PublisherEasyChair
Publication statusPublished - 16 Nov 2018

Fingerprint

Dive into the research topics of 'Lookahead-Based SMT Solving'. Together they form a unique fingerprint.

Cite this