tr-announce July 2013

tr-announce@lists.rwth-aachen.de

1 participants
1 discussions

2013-08: On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers

by Thomas Ströder

The following technical report is available from http://aib.informatik.rwth-aachen.de: On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers Sebastian Junges, Ulrich Loup, Florian Corzilius and Erika Ábrahám AIB 2013-08 We address satisfiability checking for the first-order theory of the real-closed field (RCF) using satisfiability-modulo-theories (SMT) solving. SMT solvers combine a SAT solver to resolve the Boolean structure of a given formula with theory solvers to verify the consistency of sets of theory constraints. In this paper, we report on an integration of Gröbner bases as a theory solver so that it conforms with the requirements for efficient SMT solving: (1) it allows the incremental adding and removing of polynomials from the input set and (2) it can compute an inconsistent subset of the input constraints if the Gröbner basis contains 1. We modify Buchberger's algorithm by implementing a new update operator to optimize the Gröbner basis and provide two methods to handle inequalities. Our implementation uses special data structures tuned to be efficient for huge sets of sparse polynomials. Besides solving, the resulting module can be used to simplify constraints before being passed to other RCF theory solvers based on, e.g., the cylindrical algebraic decomposition.

11 years, 2 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce July 2013