CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishMany approaches for Satisfiability Modulo Theory (SMT rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory ). When is the combination of two simpler theories, the approach is typically handled by means of Nelson-Oppen’s (NO) theory combination schema in which two specific -solver deduce and exchange (disjunctions of) interface equalities. In recent papers we have proposed a new approach to , 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 , which shows that, using state-of-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 and for both convex and non-convex theories. This work has been partly supported by ISAAC, an European sponsored project, contract no. AST3-CT-2003-501848, by ORCHID, a project sponsored by Provincia Autonoma di Trento, and by a grant from Intel Corporation.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: a Comparative Analysis. Extended version |
| Autori: | |
| Data di pubblicazione: | 2009 |
| Rivista: | |
| Abstract: | Many approaches for Satisfiability Modulo Theory (SMT rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory ). When is the combination of two simpler theories, the approach is typically handled by means of Nelson-Oppen’s (NO) theory combination schema in which two specific -solver deduce and exchange (disjunctions of) interface equalities. In recent papers we have proposed a new approach to , 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 , which shows that, using state-of-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 and for both convex and non-convex theories. This work has been partly supported by ISAAC, an European sponsored project, contract no. AST3-CT-2003-501848, by ORCHID, a project sponsored by Provincia Autonoma di Trento, and by a grant from Intel Corporation. |
| Handle: | http://hdl.handle.net/11582/4620 |
| Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
http://hdl.handle.net/11582/4620
Copyright © 2020