Incomplete SMT techniques for solving non-linear formulas over the integers

DOI10.1145/3340923MaRDI QIDQ4972164zbMATH OpenOpenAlexWikidataFDO

Authors Cristina Borralleras, Daniel Larraz, Enric Rodríguez-Carbonell, Albert Oliveras, Albert Rubio

Publication date 22 November 2019

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2008.13601

zbMATH Keywords

nonlinear arithmeticsatisfiability modulo theories

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: We present new methods for solving the Satisfiability Modulo Theories problem over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA), which consists in deciding the satisfiability of ground formulas with integer polynomial constraints. Following previous work, we propose to solve SMT(QF-NIA) instances by reducing them to linear arithmetic: non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. For variables that do not have a finite domain, we can artificially introduce one by imposing a lower and an upper bound, and iteratively enlarge it until a solution is found (or the procedure times out). The key for the success of the approach is to determine, at each iteration, which domains have to be enlarged. Previously, unsatisfiable cores were used to identify the domains to be changed, but no clue was obtained as to how large the new domains should be. Here we explain two novel ways to guide this process by analyzing solutions to optimization problems: (i) to minimize the number of violated artificial domain bounds, solved via a Max-SMT solver, and (ii) to minimize the distance with respect to the artificial domains, solved via an Optimization Modulo Theories (OMT) solver. Using this SMT-based optimization technology allows smoothly extending the method to also solve Max-SMT problems over non-linear integer arithmetic. Finally we leverage the resulting Max-SMT(QF-NIA) techniques to solve $existsforall$ formulas in a fragment of quantified non-linear arithmetic that appears commonly in verification and synthesis applications.

Recommendations

• Minimal-model-guided approaches to solving polynomial constraints and extensions
• Solving nonlinear integer arithmetic with MCSAT
• Experimenting on solving nonlinear integer arithmetic with incremental linearization
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• Solving non-linear arithmetic

Cited in

(9)

• Experimenting on solving nonlinear integer arithmetic with incremental linearization
• A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
• Solving nonlinear integer arithmetic with MCSAT
• Minimal-model-guided approaches to solving polynomial constraints and extensions
• Interpolants for Linear Arithmetic in SMT
• SMT-Solvers in Action: Encoding and Solving Selected Problems in NP and EXPTIME
• Local Search For Satisfiability Modulo Integer Arithmetic Theories
• On the complexity of convex and reverse convex prequadratic constraints
• Optimization modulo non-linear arithmetic via incremental linearization

Describes a project that uses

Uses Software

• SMT-LIB
• StarExec
• raSAT
• OptiMathSAT
• Yices
• z3
• ProB
• vZ
• CVC4
• CalCS
• EFSMT
• SMT-RAT

This page was built for publication: Incomplete SMT techniques for solving non-linear formulas over the integers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4972164)