Exploring Predictability of SAT/SMT Solvers

Robert Brummayer; Duckki Oe; Aaron Stump

Exploring Predictability of SAT/SMT Solvers

Robert Brummayer, Duckki Oe, Aaron Stump

Institute of Formal Models and Verification

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

Abstract

This paper seeks to explore the predictability of SAT and SMT solvers in response to different kinds of changes to benchmarks. We consider both semantics-preserving and possibly semanticsmodifying transformations, and provide preliminary data about solver predictability. We also propose carrying learned theory lemmas over from an original run to runs on similar benchmarks, and show the benefits of this idea as a heuristic for improving predictability of SMT solvers.

Original language	English
Title of host publication	Intl. Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (EMSQMS'10), affiliated to IJCAR'10 and CAV'10 at FLOC'10.
Number of pages	13
Publication status	Published - 2010

Fields of science

102011 Formal languages
102 Computer Sciences
101 Mathematics

JKU Focus areas

Computation in Informatics and Mathematics

Cite this

@inproceedings{2b20a947b8f9403c91c49617c2a7bd56,

title = "Exploring Predictability of SAT/SMT Solvers",

abstract = "This paper seeks to explore the predictability of SAT and SMT solvers in response to different kinds of changes to benchmarks. We consider both semantics-preserving and possibly semanticsmodifying transformations, and provide preliminary data about solver predictability. We also propose carrying learned theory lemmas over from an original run to runs on similar benchmarks, and show the benefits of this idea as a heuristic for improving predictability of SMT solvers.",

author = "Robert Brummayer and Duckki Oe and Aaron Stump",

year = "2010",

language = "English",

booktitle = "Intl. Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (EMSQMS'10), affiliated to IJCAR'10 and CAV'10 at FLOC'10.",

}

TY - GEN

T1 - Exploring Predictability of SAT/SMT Solvers

AU - Brummayer, Robert

AU - Oe, Duckki

AU - Stump, Aaron

PY - 2010

Y1 - 2010

N2 - This paper seeks to explore the predictability of SAT and SMT solvers in response to different kinds of changes to benchmarks. We consider both semantics-preserving and possibly semanticsmodifying transformations, and provide preliminary data about solver predictability. We also propose carrying learned theory lemmas over from an original run to runs on similar benchmarks, and show the benefits of this idea as a heuristic for improving predictability of SMT solvers.

AB - This paper seeks to explore the predictability of SAT and SMT solvers in response to different kinds of changes to benchmarks. We consider both semantics-preserving and possibly semanticsmodifying transformations, and provide preliminary data about solver predictability. We also propose carrying learned theory lemmas over from an original run to runs on similar benchmarks, and show the benefits of this idea as a heuristic for improving predictability of SMT solvers.

M3 - Conference proceedings

BT - Intl. Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions (EMSQMS'10), affiliated to IJCAR'10 and CAV'10 at FLOC'10.

ER -