License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.09461.3
URN: urn:nbn:de:0030-drops-25081
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2508/
Go to the corresponding Portal

Abraham, Erika ; Loup, Ulrich

SMT-Solving for the First-Order Theory of the Reals

pdf-format:
09461.AbrahamErika.Paper.2508.pdf (0.1 MB)

Abstract

SAT-solving is a highly actual research area with increasing success and plenty of industrial applications. SMT-solving, extending SAT with theories, has its main focus on linear real constrains. However, there are only few solvers going further to more expressive but still decidable logics like the first-order theory of the reals with addition and multiplication.

The main requests on theory solvers that must be fulfilled for their efficient embedding into an SMT solver are (a) incrementality, (b) the efficient computation of minimal infeasible subsets, and (c) the support of backtracking. For the first-order
theory of the reals we are not aware of any solver offering those functionalities.
In this work we address the possibilities to extend existing theory solving algorithms to come up with a theory solver suited for SMT.

BibTeX - Entry

@InProceedings{abraham_et_al:DagSemProc.09461.3,
  author =	{Abraham, Erika and Loup, Ulrich},
  title =	{{SMT-Solving for the First-Order Theory of the Reals}},
  booktitle =	{Algorithms and Applications for Next Generation SAT Solvers},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9461},
  editor =	{Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2508},
  URN =		{urn:nbn:de:0030-drops-25081},
  doi =		{10.4230/DagSemProc.09461.3},
  annote =	{Keywords: SMT-solving, first-order theory of the reals, verification}
}

Keywords: SMT-solving, first-order theory of the reals, verification
Collection: 09461 - Algorithms and Applications for Next Generation SAT Solvers
Issue Date: 2010
Date of publication: 17.03.2010

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI