Colors Make Theories Hard.

The satisfiability problem for conjunctions of quantifier-free literals in first-order theories $$\\mathcal {T}$$ of interest---\"$$\\mathcal {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 $$\\mathcal {T}$$ of interest, a key theoretical problem is to establish the computational intractability of $$\\mathcal {T}$$-solving, or to identify intractable fragments of $$\\mathcal {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 $$\\mathcal {T}$$-solving, which is based on the novel concept of \"colorer\" for a theory $$\\mathcal {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.