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].

Colors make theories hard

Sebastiani, Roberto
2016-01-01

Abstract

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.
2016
Automated Reasoning: 8th International Joint Conference IJCAR 2016 Proceedings
Cham
Springer Verlag
9783319402284
978-3-319-40229-1
Sebastiani, Roberto
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].
File in questo prodotto:
File Dimensione Formato  
ijcar16.pdf

Open Access dal 01/01/2018

Descrizione: articolo principale
Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 376.64 kB
Formato Adobe PDF
376.64 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/168325
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact