From simplification to a partial theory solver for non-linear real polynomial constraints. (September 2020)

• Record Type: Journal Article
• Authors: Brown, Christopher W.; Vale-Enriquez, Fernando
• Is Part Of: Journal of symbolic computation. Volume 100(2020)
• Page Start: 72
• Page End: 101
• Publication Date: 2020-09
• Subjects: Tarski formulas -- Formula simplification -- SMT -- Nonlinear constraints; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2019.07.020
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: Computing with non-linear polynomial constraints over the real numbers has been an important area within Computer Algebra since the field's inception. More recently, satisfiability for this theory has become an important problem in the SMT-solving community. Inspired by the S C 2 project, this paper combines ideas from both communities to produce a fast "partial solver" for the theory — i.e. a solver that can sometimes decide the satisfiability of formulas, but sometimes fails to make a determination. The partial solver is based on existing "black-box/white-box" simplification algorithms, which this paper extends to allow for the production of UNSAT cores (and stronger simplifications). The production of UNSAT cores is required if the partial solver is to be used in SMT-solving, which is one of the primary motivations for this work. The authors have implemented the partial solver in the system, and this paper also reports on experiments based on that implementation.