The Strategy Challenge in SMT Solving

Leonardo de Moura, Grant Passmore

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract / Description of output

High-performance SMT solvers contain many tightly integrated, hand-crafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform badly on classes of problems not anticipated by solver developers. This issue is becoming increasingly pressing as SMT solvers begin to gain the attention of practitioners in diverse areas of science and engineering. We present a challenge to the SMT community: to develop methods through which users can exert strategic control over core heuristic aspects of SMT solvers. We present evidence that the adaptation of ideas of strategy prevalent both within the Argonne and LCF theorem proving paradigms can go a long way towards realizing this goal.
Original languageEnglish
Title of host publicationAutomated Reasoning and Mathematics
Subtitle of host publicationEssays in Memory of William W. McCune
EditorsMariaPaola Bonacina, MarkE. Stickel
PublisherSpringer Berlin Heidelberg
Pages15-44
Number of pages30
Volume7788
ISBN (Electronic)978-3-642-36675-8
ISBN (Print)978-3-642-36674-1
DOIs
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume7788

Fingerprint

Dive into the research topics of 'The Strategy Challenge in SMT Solving'. Together they form a unique fingerprint.

Cite this