Quantified Constraints and Containment Problems
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2015-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1585/pdf |
| _version_ | 1811225329539219456 |
|---|---|
| author | Barnaby D. Martin Hubie Chen Florent R. Madelaine |
| author_facet | Barnaby D. Martin Hubie Chen Florent R. Madelaine |
| author_sort | Barnaby D. Martin |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-12T09:05:14Z |
| format | Article |
| id | doaj.art-bcc2978e80334da59593dc95b1a12565 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-12T09:05:14Z |
| publishDate | 2015-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-bcc2978e80334da59593dc95b1a125652022-12-22T03:39:07ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742015-09-01Volume 11, Issue 310.2168/LMCS-11(3:9)20151585Quantified Constraints and Containment ProblemsBarnaby D. MartinHubie ChenFlorent R. MadelaineThe 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.https://lmcs.episciences.org/1585/pdfcomputer science - logic in computer science |
| spellingShingle | Barnaby D. Martin Hubie Chen Florent R. Madelaine Quantified Constraints and Containment Problems Logical Methods in Computer Science computer science - logic in computer science |
| title | Quantified Constraints and Containment Problems |
| title_full | Quantified Constraints and Containment Problems |
| title_fullStr | Quantified Constraints and Containment Problems |
| title_full_unstemmed | Quantified Constraints and Containment Problems |
| title_short | Quantified Constraints and Containment Problems |
| title_sort | quantified constraints and containment problems |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/1585/pdf |
| work_keys_str_mv | AT barnabydmartin quantifiedconstraintsandcontainmentproblems AT hubiechen quantifiedconstraintsandcontainmentproblems AT florentrmadelaine quantifiedconstraintsandcontainmentproblems |