Summary: | The quantified constraint satisfaction problem $\mathrm{QCSP}(\mathcal{A})$
is the problem to decide whether a positive Horn sentence, involving nothing
more than the two quantifiers and conjunction, is true on some fixed structure
$\mathcal{A}$. We study two containment problems related to the QCSP. Firstly,
we give a combinatorial condition on finite structures $\mathcal{A}$ and
$\mathcal{B}$ that is necessary and sufficient to render
$\mathrm{QCSP}(\mathcal{A}) \subseteq \mathrm{QCSP}(\mathcal{B})$. We prove
that $\mathrm{QCSP}(\mathcal{A}) \subseteq \mathrm{QCSP}(\mathcal{B})$, that is
all sentences of positive Horn logic true on $\mathcal{A}$ are true on
$\mathcal{B}$, iff there is a surjective homomorphism from
$\mathcal{A}^{|A|^{|B|}}$ to $\mathcal{B}$. This can be seen as improving an
old result of Keisler that shows the former equivalent to there being a
surjective homomorphism from $\mathcal{A}^\omega$ to $\mathcal{B}$. We note
that this condition is already necessary to guarantee containment of the
$\Pi_2$ restriction of the QCSP, that is $\Pi_2$-$\mathrm{CSP}(\mathcal{A})
\subseteq \Pi_2$-$\mathrm{CSP}(\mathcal{B})$. The exponent's bound of
${|A|^{|B|}}$ places the decision procedure for the model containment problem
in non-deterministic double-exponential time complexity. We further show the
exponent's bound $|A|^{|B|}$ to be close to tight by giving a sequence of
structures $\mathcal{A}$ together with a fixed $\mathcal{B}$, $|B|=2$, such
that there is a surjective homomorphism from $\mathcal{A}^r$ to $\mathcal{B}$
only when $r \geq |A|$. Secondly, we prove that the entailment problem for
positive Horn fragment of first-order logic is decidable. That is, given two
sentences $\varphi$ and $\psi$ of positive Horn, we give an algorithm that
determines whether $\varphi \rightarrow \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.
|