Details:
Title  On Gr\"obner bases in the context of satisfiabilitymodulotheories solving over the real numbers.  Author(s)  Erika Abraham, Florian Corzilius, Sebastian Junges, Ulrich Loup  Type  Book, Chapter in Book, Conference Proceeding  Abstract  e address satisfiability checking for the firstorder theory of the realclosed field (RCF) using satisfiabilitymodulotheories (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.  ISBN  9783642406621/pbk 
URL 
http://link.springer.com/chapter/10.1007%2F9783642406638_18 
Language  English  Pages  186198  Publisher  Berlin: Springer  Year  2013  Edition  0  Translation 
No  Refereed 
No 
