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 Grobner 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 Groebner basis contains 1. We modify Buchberger's algorithm by implementing a new update operator to optimize the Groebner 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.
展开▼
