Many approaches for Satisfiability Modulo Theory (SMT(T)) rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory T (T-solver). When T is the combination T1 U T2 of two simpler theories, the approach is typically handled by means of Nelson-Oppen’s (NO) theory combination schema in which two specific T -solvers deduce and exchange (disjunctions of) interface equalities. In recent papers we have proposed a new approach to SMT(T1 U T2), called Delayed Theory Combination (DTC). Here part or all the (possibly very expensive) task of deducing interface equalities is played by the SAT solver itself, at the potential cost of an enlargement of the boolean search space. In principle this enlargement could be up to exponential in the number of interface equalities generated. In this paper we show that this estimate was too pessimistic. We present a comparative analysis of DTC vs. NO for SMT(T1 U T2), which shows that, using stateof-the-art SAT-solving techniques, the amount of boolean branches performed by DTC can be upper bounded by the number of deductions and boolean branches performed by NO on the same problem. We prove the result for different deduction capabilities of the T-solvers and for both convex and non-convex theories.

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis / Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto. - ELETTRONICO. - (2006), pp. 1-23.

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis

Bruttomesso, Roberto;Cimatti, Alessandro;Griggio, Alberto;Sebastiani, Roberto
2006-01-01

Abstract

Many approaches for Satisfiability Modulo Theory (SMT(T)) rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory T (T-solver). When T is the combination T1 U T2 of two simpler theories, the approach is typically handled by means of Nelson-Oppen’s (NO) theory combination schema in which two specific T -solvers deduce and exchange (disjunctions of) interface equalities. In recent papers we have proposed a new approach to SMT(T1 U T2), called Delayed Theory Combination (DTC). Here part or all the (possibly very expensive) task of deducing interface equalities is played by the SAT solver itself, at the potential cost of an enlargement of the boolean search space. In principle this enlargement could be up to exponential in the number of interface equalities generated. In this paper we show that this estimate was too pessimistic. We present a comparative analysis of DTC vs. NO for SMT(T1 U T2), which shows that, using stateof-the-art SAT-solving techniques, the amount of boolean branches performed by DTC can be upper bounded by the number of deductions and boolean branches performed by NO on the same problem. We prove the result for different deduction capabilities of the T-solvers and for both convex and non-convex theories.
2006
Trento
Università degli Studi di Trento - Dipartimento di Informatica e Telecomunicazioni
Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis / Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto. - ELETTRONICO. - (2006), pp. 1-23.
Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto
File in questo prodotto:
File Dimensione Formato  
032.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 310.85 kB
Formato Adobe PDF
310.85 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/358075
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact