Colors make theories hard

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.