King's College London

Research portal

Lookahead-Based SMT Solving

Research output: Chapter in Book/Report/Conference proceedingConference paper

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

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

Documents

  • HyvarinenMSCS_LPAR2018

    HyvarinenMSCS_LPAR2018.pdf, 922 KB, application/pdf

    8/11/2018

    Accepted author manuscript

    Other

King's Authors

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.

Download statistics

No data available

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454