Quantified Constraints and Containment Problems

This paper is a considerably expanded journal version of a LICS 2008 paper of the same title together with the most significant parts of a CP 2012 paper from the latter two authorsThe quantified constraint satisfaction problem QCSP(A) is the problem to decide whether a positive Horn (pH) sentence, involving nothing more than the two quantifiers and conjunction, is true on some fixed structure A. We study two containment problems related to the QCSP. Firstly, we give a combinatorial condition on finite structures A and B that characterises QCSP(A) subset of QCSP(B). We prove that QCSP(A) subset of QCSP(B), i.e. all sentences of pH true on A are true on B, iff there is a surjective homomorphism from A^{|A|^{|B|}} to B. This can be seen as improving an old result of Keisler that shows the former equivalent to there being a surjective homomorphism from A^omega to B. We note that this condition is already necessary to guarantee containment of the Pi_2 restriction of the QCSP. The exponent's bound of |A|^{|B|} places the decision procedure for the model containment problem in non-deterministic double-exponential time. We further show the bound |A|^{|B|} to be close to tight by giving a sequence of structures A together with a fixed B, |B|=2, such that there is a surjective homomorphism from A^r to B only when r is greater than or equal to |A|. Secondly, we prove that the entailment problem for pH is decidable. That is, given two sentences phi and psi of positive Horn, we give an algorithm that determines whether phi implies psi is true in all structures (models). Our result is in some sense tight, since we show that the entailment problem for positive first-order logic (i.e. positive Horn plus disjunction) is undecidable. In the final part of the paper we ponder a notion of Q-core that is some canonical representative among the class of templates that engender the same QCSP. Although the Q-core is not as well-behaved as its better known cousin the core, we demonstrate that it is still a useful notion in the realm of QCSP complexity classifications