CINECA IRIS Institutional Research Information System
IRIS è l'Anagrafe della ricerca dell'Università degli Studi di Trento, e ha lo scopo di raccogliere, documentare, conservare e diffondere, anche ad accesso aperto, la produzione scientifica degli autori afferenti all'Università degli Studi di Trento.
EnglishThe satisfiability problem for conjunctions of quantifier-free literals in first-order theories T of interest–“T -solving” for short–has been deeply investigated for more than three decades from both theoretical and practical perspectives, and it is currently a core issue of state-of-the-art SMT solving. Given some theory T of interest, a key theoretical problem is to establish the computational (in)tractability of T-solving, or to identify intractable fragments of T. In this paper we investigate this problem from a general perspective, and we present a simple and general criterion for establishing the NP-hardness of T-solving, which is based on the novel concept of “colorer” for a theory T. As a proof of concept, we show the effectiveness and simplicity of this novel criterion by easily producing very simple proofs of the NP-hardness for many theories of interest for SMT, or of some of their fragments.
Colors make theories hard / Sebastiani, Roberto. - STAMPA. - 9706:(2016), pp. 152-170. ((Intervento presentato al convegno IJCAR 2016 tenutosi a Coimbra, Portugal nel 27th June-2nd July 2016 [10.1007/978-3-319-40229-1_11].
| Titolo: | Colors make theories hard | |
| Autori: | Sebastiani, Roberto | |
| Autori Unitn: | ||
| Titolo del volume contenente il saggio: | Automated Reasoning: 8th International Joint Conference IJCAR 2016 Proceedings | |
| Luogo di edizione: | Cham | |
| Casa editrice: | Springer Verlag | |
| Anno di pubblicazione: | 2016 | |
| Codice identificativo Scopus: | 2-s2.0-84976610701 | |
| Codice identificativo WOS: | WOS:000491484800011 | |
| ISBN: | 9783319402284 978-3-319-40229-1 | |
| Handle: | http://hdl.handle.net/11572/168325 | |
| Citazione: | Colors make theories hard / Sebastiani, Roberto. - STAMPA. - 9706:(2016), pp. 152-170. ((Intervento presentato al convegno IJCAR 2016 tenutosi a Coimbra, Portugal nel 27th June-2nd July 2016 [10.1007/978-3-319-40229-1_11]. | |
| Appare nelle tipologie: | 04.1 Saggio in atti di convegno (Paper in Proceedings) |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| ijcar16.pdf | articolo principale | Post-print referato (Refereed author’s manuscript) | Tutti i diritti riservati (All rights reserved) | Open Access Visualizza/Apri |
http://hdl.handle.net/11572/168325
Copyright © 2022