Search
Incomplete SMT techniques for solving non-linear formulas over the integers
Borralleras C., Larraz D., Rodríguez-Carbonell E., Oliveras A., Rubio A.  ACM Transactions on Computational Logic 20 (4): 1-36, 2019. Type: Article
 Date Reviewed: May 27 2021
 It is well known that nonlinear integer arithmetic is undecidable due to a negative answer to Hilbert’s tenth problem. Still, constraint solving over nonlinear integer polynomials has attracted considerable attention because of the wide range of applications. Obviously, the existing solving methods are incomplete. Recent approaches exploit the progress made in Boolean satisfiability problem (SAT)/satisfiability modulo theories (SMT) technology, and so does the approach described in this paper. It addresses “the satisfiability of first-order quantifier-free formulas where atoms are polynomial inequalities over integer variables,” and extends an earlier approach proposed by the same authors [1]. In that previous work, the problem is solved by reducing it to “the satisfiability modulo theory of quantifier-free linear integer arithmetic.” The reduction idea is to linearize nonlinear monomials, “[replacing] them with fresh variables and by performing case splitting on integer variables with finite domain[s].” However, the domains of some variables may be infinite. In that case, the method artificially fixes lower and upper bounds for those domains. A problem with artificial bounds is that an underlying SMT solver (for quantifier-free linear integer arithmetic) might not be able to solve the obtained formula. In that case, the bounds are relaxed. This is not done blindly: a technique of domain enlargement described in [1] suggests which bounds should be weakened. However, it does not say “how large the new domains have to be made,” which undermines the efficiency of the approach. The authors address this problem here. Borralleras et al. propose new strategies for domain enlargement based on minimal models. The idea is “to replace the satisfiability check in linear arithmetic with an optimization call.” The models assign values to variables. Among all models of linearization, the linear solver should select “the best one,” that is, “the one that is closest to being a solution to the original nonlinear formula” (“according to a certain cost function”). If the selected model does not satisfy the nonlinear formula, then the bounds are weakened so that the enlarged domains include those values which were violating the formula. Two concrete cost functions are considered, and the corresponding approaches to domain enlargement are analyzed and evaluated. Next, the authors extend their techniques from SMT solving to Max-SMT solving for quantifier-free nonlinear integer arithmetic (which is useful for termination and nontermination proving and safety analysis). A further extension concerns a “fragment of the first-order theory of nonlinear real and integer arithmetic.” In this fragment, formulas are of the form ∃ x ∀ y F(x,y), where F is a quantifier-free formula over polynomial inequalities, existential variables have integer type, universal variables have real type, and monomials do not “contain the product of two universally quantified variables.” Such a fragment appears in certain kinds of verification and synthesis problems. The authors describe techniques for solving SAT and Max-SAT problems in this fragment. The methods introduced in the paper are incomplete: unsatisfiable instances might not be detected. Therefore, the goal was to develop techniques that help to solve satisfiable formulas efficiently. The experimental results illustrate the proposed approach’s potential. It is a well-written paper. The results are valuable to the SAT/SMT community. Reviewer:  Temur Kutsia Review #: CR147274 (2108-0214)
 1) Borralleras, C.; Lucas, S.; Oliveras, A.; Rodríguez-Carbonell, E.; Rubio, A. SAT modulo linear arithmetic for solving polynomial constraints. Journal of Automated Reasoning 48, 1(2012), 107–131.
 Would you recommend this review? yes no
 Other reviews under "General": Date On the foundations of computingPrimiero G.,  Oxford University Press, Oxford, UK, 2020. 320 pp. Type: Book (978-0-198835-65-3) Aug 12 2021 Logical methods: the art of thinking abstractly and mathematicallyAntonsen R.,  Springer, New York, NY, 2021. 304 pp. Type: Book (978-3-030637-76-7) Jul 27 2021 randUTV: a blocked randomized algorithm for computing a rank-revealing UTV factorizationMartinsson P., Quintana-Ortí G., Heavner N.  ACM Transactions on Mathematical Software 45(1): 1-26, 2019. Type: Article Jul 12 2021 more...

E-Mail This Printer-Friendly
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2022 ThinkLoud, Inc.