Lookahead-Based SMT Solving

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

Lookahead-Based SMT Solving

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

Universita della Svizzera Italiana

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

2 Citations (Scopus)

145 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 language	English
Title of host publication	LPAR-22
Subtitle of host publication	LPAR-22: 22ND INTERNATIONAL CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE AND REASONING
Publisher	EasyChair
Publication status	Published - 16 Nov 2018

Access to Document

HyvarinenMSCS_LPAR2018Accepted author manuscript, 922 KBLicence: Other

Cite this

@inbook{40c4baf1423d47d6b59d9b6b5fe4cdc9,

title = "Lookahead-Based SMT Solving",

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.",

author = "Antti Hyyvarinen and Matteo Marescotti and Parvin Sadigova and Hana Chockler and Natasha Sharygina",

year = "2018",

month = nov,

day = "16",

language = "English",

booktitle = "LPAR-22",

publisher = "EasyChair",

}

TY - CHAP

T1 - Lookahead-Based SMT Solving

AU - Hyyvarinen, Antti

AU - Marescotti, Matteo

AU - Sadigova, Parvin

AU - Chockler, Hana

AU - Sharygina, Natasha

PY - 2018/11/16

Y1 - 2018/11/16

N2 - 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.

AB - 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.

M3 - Conference paper

BT - LPAR-22

PB - EasyChair

ER -

Lookahead-Based SMT Solving

Abstract

Access to Document

Fingerprint

Cite this