The 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 |