Ir al contenido (pulsa Retorno)

Universitat Politècnica de Catalunya

    • Català
    • Castellano
    • English
    • LoginRegisterLog in (no UPC users)
  • mailContact Us
  • world English 
    • Català
    • Castellano
    • English
  • userLogin   
      LoginRegisterLog in (no UPC users)

UPCommons. Global access to UPC knowledge

Banner header
60.662 UPC E-Prints
You are here:
View Item 
  •   DSpace Home
  • E-prints
  • Departaments
  • Departament de Ciències de la Computació
  • Articles de revista
  • View Item
  •   DSpace Home
  • E-prints
  • Departaments
  • Departament de Ciències de la Computació
  • Articles de revista
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

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

Thumbnail
View/Open
journal.pdf (424,9Kb)
Share:
 
 
10.1145/3340923
 
  View Usage Statistics
Cita com:
hdl:2117/177600

Show full item record
Borralleras Andreu, Cristina
Larraz Hurtado, DanielMés informació
Rodríguez Carbonell, EnricMés informacióMés informacióMés informació
Oliveras Llunell, AlbertMés informacióMés informacióMés informació
Rubio Gimeno, AlbertoMés informacióMés informació
Document typeArticle
Defense date2019-08-01
Rights accessOpen Access
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder
ProjectAUTAR - A Unified Theory of Algorithmic Relaxations (EC-H2020-648276)
SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA (MINECO-TIN2015-69175-C4-3-R)
RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES (AEI-RTI2018-094403-B-C33)
Abstract
We present new methods for solving the Satisfiability Modulo Theories problem over the theory of QuantifierFree Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of 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 ∃∀ formulas in a fragment of quantified non-linear arithmetic that appears commonly in verification and synthesis applications.
CitationBorralleras, C. [et al.]. Incomplete SMT techniques for solving non-linear formulas over the integers. "ACM transactions on computational logic", 1 Agost 2019, vol. 20, núm. 4, article 25, p. 25:1-25:36. 
URIhttp://hdl.handle.net/2117/177600
DOI10.1145/3340923
ISSN1529-3785
Publisher versionhttps://dl.acm.org/doi/10.1145/3340923
Collections
  • Departament de Ciències de la Computació - Articles de revista [974]
  • LOGPROG - Lògica i Programació - Articles de revista [16]
Share:
 
  View Usage Statistics

Show full item record

FilesDescriptionSizeFormatView
journal.pdf424,9KbPDFView/Open

Browse

This CollectionBy Issue DateAuthorsOther contributionsTitlesSubjectsThis repositoryCommunities & CollectionsBy Issue DateAuthorsOther contributionsTitlesSubjects

© UPC Obrir en finestra nova . Servei de Biblioteques, Publicacions i Arxius

info.biblioteques@upc.edu

  • About This Repository
  • Contact Us
  • Send Feedback
  • Privacy Settings
  • Inici de la pàgina