Search

Let A be an idempotent algebra on a 3-element domain D that omits a G-set for a factor. Suppose A is not \alpha\beta-projective (for some alpha, beta subsets of D) and is not collapsible. It follows that A is switchable. We prove that, for every finite subset Delta of Inv(A), Pol(Delta) is collapsible. We also exhibit an algebra that is collapsible from a non-singleton source but is not collapsible from any singleton source.

Using a SAT-solver on top of a partial previously-known solution we improve the upper bound of the packing chromatic number of the infinite square lattice from 17 to 15. We discuss the merits of SAT-solving for this kind of problem as well as compare the performance of different encodings. Further, we improve the lower bound from 12 to 13 again using a SAT-solver, demonstrating the versatility of this technology for our approach.

We study interactions between Skolem Arithmetic and certain classes of Constraint Satisfaction Problems (CSPs). We revisit results of Glass er et al. in the context of CSPs and settle the major open question from that paper, finding a certain satisfaction problem on circuits to be decidable. This we prove using the decidability of Skolem Arithmetic. We continue by studying first-order expansions of Skolem Arithmetic without constants, (N;*), where * indicates multiplication, as CSPs. We find already here a rich landscape of problems with non-trivial instances that are in P as well as those that are NP-complete.

A discrete temporal constraint satisfaction problem is a constraint satisfaction problem (CSP) whose constraint language consists of relations that are first-order definable over $(\Bbb Z,<)$. Our main result says that every distance CSP is in Ptime or NP-complete, unless it can be formulated as a finite domain CSP in which case the computational complexity is not known in general., Comment: 41 pages

Inspired by computational complexity results for the quantified constraint satisfaction problem, we study the clones of idempotent polymorphisms of certain digraph classes. Our first results are two algebraic dichotomy, even "gap", theorems. Building on and extending [Martin CP'11], we prove that partially reflexive paths bequeath a set of idempotent polymorphisms whose associated clone algebra has: either the polynomially generated powers property (PGP); or the exponentially generated powers property (EGP). Similarly, we build on [DaMM ICALP'14] to prove that semicomplete digraphs have the same property. These gap theorems are further motivated by new evidence that PGP could be the algebraic explanation that a QCSP is in NP even for unbounded alternation. Along the way we also effect a study of a concrete form of PGP known as collapsibility, tying together the algebraic and structural threads from [Chen Sicomp'08], and show that collapsibility is equivalent to its $\Pi_2$-restriction. We also give a decision procedure for $k$-collapsibility from a singleton source of a finite structure (a form of collapsibility which covers all known examples of PGP for finite structures). Finally, we present a new QCSP trichotomy result, for partially reflexive paths with constants. Without constants it is known these QCSPs are either in NL or Pspace-complete [Martin CP'11], but we prove that with constants they attain the three complexities NL, NP-complete and Pspace-complete.

We study constraint satisfaction problems (CSPs) in the presence of counting quantifiers $\exists^{\geq j}$, asserting the existence of $j$ distinct witnesses for the variable in question. As a continuation of our previous (CSR 2012) paper, we focus on the complexity of undirected graph templates. As our main contribution, we settle the two principal open questions proposed in (CSR 2012). Firstly, we complete the classification of clique templates by proving a full trichotomy for all possible combinations of counting quantifiers and clique sizes, placing each case either in P, NP-complete or Pspace-complete. This involves resolution of the cases in which we have the single quantifier $\exists^{\geq j}$ on the clique $K_{2j}$. Secondly, we confirm a conjecture from (CSR 2012), which proposes a full dichotomy for $\exists$ and $\exists^{\geq 2}$ on all finite undirected graphs. The main thrust of this second result is the solution of the complexity for the infinite path which we prove is a polynomial-time solvable problem. By adapting the algorithm for the infinite path we are then able to solve the problem for finite paths, and then trees and forests. Thus as a corollary to this work, combining with the other cases from (CSR 2012), we obtain a full dichotomy for $\exists$ and $\exists^{\geq 2}$ quantifiers on finite graphs, each such problem being either in P or NP-hard. Finally, we persevere with the work of (CSR 2012) in exploring cases in which there is dichotomy between P and Pspace-complete, in contrast with situations in which the intermediate NP-completeness may appear.

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., Comment: 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 authors

We provide a number of simplified and improved separations between pairs of Resolution-with-bounded-conjunction refutation systems, Res(d), as well as their tree-like versions, Res*(d). The contradictions we use are natural combinatorial principles: the Least number principle, LNP_n and an ordered variant thereof, the Induction principle, IP_n. LNP_n is known to be easy for Resolution. We prove that its relativisation is hard for Resolution, and more generally, the relativisation of LNP_n iterated d times provides a separation between Res(d) and Res(d+1). We prove the same result for the iterated relativisation of IP_n, where the tree-like variant Res*(d) is considered instead of Res(d). We go on to provide separations between the parameterized versions of Res(1) and Res(2). Here we are able again to use the relativisation of the LNP_n, but the classical proof breaks down and we are forced to use an alternative. Finally, we separate the parameterized versions of Res*(1) and Res*(2). Here, the relativisation of IP_n will not work as it is, and so we make a vectorising amendment to it in order to address this shortcoming

We study the (non-uniform) quantified constraint satisfaction problem QCSP(H) as H ranges over partially reflexive cycles. We obtain a complexity-theoretic dichotomy: QCSP(H) is either in NL or is NP-hard. The separating conditions are somewhat esoteric hence the epithet "wavy line of tractability"., Comment: Extended abstract at CSR 2013

The model checking problem for various fragments of first-order logic has attracted much attention over the last two decades: in particular, for the primitive positive and the positive Horn fragments, which are better known as the constraint satisfaction problem and the quantified constraint satisfaction problem, respectively. These two fragments are in fact the only ones for which there is currently no known complexity classification. All other syntactic fragments can be easily classified, either directly or using Schaefer's dichotomy theorems for SAT and QSAT, with the exception of the positive equality free fragment. This outstanding fragment can also be classified and enjoys a tetrachotomy: according to the model, the corresponding model checking problem is either tractable, NP-complete, co-NP-complete or Pspace-complete. Moreover, the complexity drop is always witnessed by a generic solving algorithm which uses quantifier relativisation. Furthermore, its complexity is characterised by algebraic means: the presence or absence of specific surjective hyper-operations among those that preserve the model characterise the complexity.

The constraint satisfaction problem (CSP) and its quantified extensions, whether without (QCSP) or with disjunction (QCSP_or), correspond naturally to the model checking problem for three increasingly stronger fragments of positive first-order logic. Their complexity is often studied when parameterised by a fixed model, the so-called template. It is a natural question to ask when two templates are equivalent, or more generally when one "contain" another, in the sense that a satisfied instance of the first will be necessarily satisfied in the second. One can also ask for a smallest possible equivalent template: this is known as the core for CSP. We recall and extend previous results on containment, equivalence and "coreness" for QCSP_or before initiating a preliminary study of cores for QCSP which we characterise for certain structures and which turns out to be more elusive.

We provide separations between the parameterized versions of Res(1) (Resolution) and Res(2). Using a different set of parameterized contradictions, we also separate the parameterized versions of Res*(1) (tree-Resolution) and Res*(2).

The Surjective Homomorphism problem is to test whether a given graph G called the guest graph allows a vertex-surjective homomorphism to some other given graph H called the host graph. The bijective and injective homomorphism problems can be formulated in terms of spanning subgraphs and subgraphs, and as such their computational complexity has been extensively studied. What about the surjective variant? Because this problem is NP-complete in general, we restrict the guest and the host graph to belong to graph classes G and H, respectively. We determine to what extent a certain choice of G and H influences its computational complexity. We observe that the problem is polynomial-time solvable if H is the class of paths, whereas it is NP-complete if G is the class of paths. Moreover, we show that the problem is even NP-complete on many other elementary graph classes, namely linear forests, unions of complete graphs, cographs, proper interval graphs, split graphs and trees of pathwidth at most 2. In contrast, we prove that the problem is fixed-parameter tractable in k if G is the class of trees and H is the class of trees with at most k leaves, or if G and H are equal to the class of graphs with vertex cover number at most k., Comment: 13 pages, 5 figures

We initiate a program of parameterized proof complexity that aims to provide evidence that FPT is different from W[1]. A similar program already exists for the classes W[2] and W[SAT]. We contrast these programs and prove upper and lower bounds for W[1]-parameterized Resolution.

We initiate the study of constraint satisfaction problems (CSPs) in the presence of counting quantifiers, which may be seen as variants of CSPs in the mould of quantified CSPs (QCSPs). We show that a single counting quantifier strictly between exists^1:=exists and exists^n:=forall (the domain being of size n) already affords the maximal possible complexity of QCSPs (which have both exists and forall), being Pspace-complete for a suitably chosen template. Next, we focus on the complexity of subsets of counting quantifiers on clique and cycle templates. For cycles we give a full trichotomy -- all such problems are in L, NP-complete or Pspace-complete. For cliques we come close to a similar trichotomy, but one case remains outstanding. Afterwards, we consider the generalisation of CSPs in which we augment the extant quantifier exists^1:=exists with the quantifier exists^j (j not 1). Such a CSP is already NP-hard on non-bipartite graph templates. We explore the situation of this generalised CSP on bipartite templates, giving various conditions for both tractability and hardness -- culminating in a classification theorem for general graphs. Finally, we use counting quantifiers to solve the complexity of a concrete QCSP whose complexity was previously open.

We survey known results about the complexity of surjective homomorphism problems, studied in the context of related problems in the literature such as list homomorphism, retraction and compaction. In comparison with these problems, surjective homomorphism problems seem to be harder to classify and we examine especially three concrete problems that have arisen from the literature, two of which remain of open complexity.

For a connected graph G=(V,E), a subset U of V is called a disconnected cut if U disconnects the graph and the subgraph induced by U is disconnected as well. We show that the problem to test whether a graph has a disconnected cut is NP-complete. This problem is polynomially equivalent to the following problems: testing if a graph has a 2K2-partition, testing if a graph allows a vertex-surjective homomorphism to the reflexive 4-cycle and testing if a graph has a spanning subgraph that consists of at most two bicliques. Hence, as an immediate consequence, these three decision problems are NP-complete as well. This settles an open problem frequently posed in each of the four settings., Comment: Conference version appeared at CP 2011. To appear JCTB (DOI: 10.1016/j.jctb.2014.09.002)

We study the (non-uniform) quantified constraint satisfaction problem QCSP(H) as H ranges over partially reflexive forests. We obtain a complexity-theoretic dichotomy: QCSP(H) is either in NL or is NP-hard. The separating condition is related firstly to connectivity, and thereafter to accessibility from all vertices of H to connected reflexive subgraphs. In the case of partially reflexive paths, we give a refinement of our dichotomy: QCSP(H) is either in NL or is Pspace-complete.

Building on a result of Larose and Tesson for constraint satisfaction problems (CSP s), we uncover a dichotomy for the quantified constraint satisfaction problem QCSP(B), where B is a finite structure that is a core. Specifically, such problems are either in ALogtime or are L-hard. This involves demonstrating that if CSP(B) is first-order expressible, and B is a core, then QCSP(B) is in ALogtime. We show that the class of B such that CSP(B) is first-order expressible (indeed, trivially true) is a microcosm for all QCSPs. Specifically, for any B there exists a C such that CSP(C) is trivially true, yet QCSP(B) and QCSP(C) are equivalent under logspace reductions.

We study the complexity of constraint satisfaction problems for templates $\Gamma$ that are first-order definable in $(\Bbb Z; succ)$, the integers with the successor relation. Assuming a widely believed conjecture from finite domain constraint satisfaction (we require the tractability conjecture by Bulatov, Jeavons and Krokhin in the special case of transitive finite templates), we provide a full classification for the case that Gamma is locally finite (i.e., the Gaifman graph of $\Gamma$ has finite degree). We show that one of the following is true: The structure Gamma is homomorphically equivalent to a structure with a d-modular maximum or minimum polymorphism and $\mathrm{CSP}(\Gamma)$ can be solved in polynomial time, or $\Gamma$ is homomorphically equivalent to a finite transitive structure, or $\mathrm{CSP}(\Gamma)$ is NP-complete., Comment: 35 pages, 2 figures

We study the complexity of evaluating positive equality-free sentences of first-order (FO) logic over a fixed, finite structure B. This may be seen as a natural generalisation of the non-uniform quantified constraint satisfaction problem QCSP(B). We introduce surjective hyper-endomorphisms and use them in proving a Galois connection that characterises definability in positive equality-free FO. Through an algebraic method, we derive a complete complexity classification for our problems as B ranges over structures of size at most three. Specifically, each problem is either in Logspace, is NP-complete, is co-NP-complete or is Pspace-complete.

The universal-algebraic approach has proved a powerful tool in the study of the complexity of CSPs. This approach has previously been applied to the study of CSPs with finite or (infinite) omega-categorical templates, and relies on two facts. The first is that in finite or omega-categorical structures A, a relation is primitive positive definable if and only if it is preserved by the polymorphisms of A. The second is that every finite or omega-categorical structure is homomorphically equivalent to a core structure. In this paper, we present generalizations of these facts to infinite structures that are not necessarily omega-categorical. (This abstract has been severely curtailed by the space constraints of arXiv -- please read the full abstract in the article.) Finally, we present applications of our general results to the description and analysis of the complexity of CSPs. In particular, we give general hardness criteria based on the absence of polymorphisms that depend on more than one argument, and we present a polymorphism-based description of those CSPs that are first-order definable (and therefore can be solved in polynomial time)., Comment: Extended abstract appeared at 25th Symposium on Logic in Computer Science (LICS 2010). This version will appear in the LMCS special issue associated with LICS 2010

We study the model checking problem, for fixed structures A, over positive equality-free first-order logic -- a natural generalisation of the non-uniform quantified constraint satisfaction problem QCSP(A). We prove a complete complexity classification for this problem when A ranges over 1.) boolean structures and 2.) digraphs of size (less than or equal to) three. The former class displays dichotomy between Logspace and Pspace-complete, while the latter class displays tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete.

We introduce QUEENS, a derivative chess problem based on the classical n-queens problem. We prove that QUEENS is NP-complete, with respect to polynomial-time reductions.

We study the complexity of the model checking problem, for fixed model A, over certain fragments L of first-order logic. These are sometimes known as the expression complexities of L. We obtain various complexity classification theorems for these logics L as each ranges over models A, in the spirit of the dichotomy conjecture for the Constraint Satisfaction Problem -- which itself may be seen as the model checking problem for existential conjunctive positive first-order logic.