Generic Expression Hardness Results for Primitive Positive Formula Comparison
This is joint work with S. Bova and M. Valeriote.
We study the expression complexity of two basic problems involving the comparison of primitive positive formulas: equivalence and containment. In particular, we study the complexity of these problems relative to finite relational structures. We present two generic hardness results for the studied problems. First, we show that on a structure B whose algebra’s variety admits the unary type, the two problems are Π2-hard. Second, we show that on a structure B whose variety is not congruence modular, the two problems are coNP-hard. As we will discuss, the first result is optimal and yields a coNP/Π2-hard dichotomy under the CSP G-set conjecture, and the second result is optimal and yields a P/coNP-hard dichotomy under the Edinburgh conjecture. Under both of the conjectures, our results thus completely resolve the complexity of the two studied problems on all finite
structures, yielding a P/coNP-complete/Π2-complete trichotomy. As far as we know, this is the first time that computational hardness results have been presented based on either of the two algebraic conditions treatment. We plan to discuss the possibility of applying our techniques to other computational problems.