-
J9
QCSP
Florent R. Madelaine and Barnaby Martin.
On the complexity of the model checking problem.
SIAM J. Comput. 47(3), 2018.
Extended version of
C10 and earlier conference papers by
Barnaby Martin, which subsumes
J6
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.
-
J8
QCSP
Hubie Chen, Florent R. Madelaine, and Barnaby Martin.
Quantified constraints and containment problems.
Logical Methods in Computer Science, 11(3), 2015.
This paper is a considerably expanded journal version of the LICS
2008 paper
C6 of the same title together with the most significant
parts of a CP 2012 paper
C13 from the latter two authors.
The 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ω to B. We note that
this condition is already necessary to guarantee
containment of the Π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 Ar 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 φ
and ψ of positive Horn, we give an algorithm
that determines whether φ implies ψ 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.
-
J7
QCSP
Barnaby Martin, Florent R. Madelaine, and Juraj Stacho.
Constraint satisfaction with counting quantifiers.
SIAM J. Discrete Math., 29(2):1065--1113, 2015.
Journal version of
C12 and a subsequent conference paper by
the first and third author.
We initiate the study of constraint satisfaction problems (CSPs) in the presence of counting quantifiers there exists>=j which assert the existence of at least j elements such that the ensuing property holds. These are natural variants of CSPs in the mould of quantified CSPs (QCSPs). Namely, there exists>=1:=there exists and there exists>=n:=for all (for the domain of size n). We observe that a single counting quantifier there exists>=j strictly between there exists and for all already affords the maximal possible complexity of QCSPs (which have both there exists and for all), namely, being Pspace-complete for a suitably chosen template. Therefore, to better understand the complexity of this problem, we focus on restricted cases for which we derive the following results. First, for all subsets of counting quantifiers on clique and cycle templates, we give a full trichotomy---all such problems are in P, NP-complete, or Pspace-complete. Second, we consider the problem with exactly two quantifiers: there exists>=1:=there exists and there exists>=j (j <>1). Such a CSP is already NP-hard on nonbipartite graph templates. We explore the situation of this generalized CSP on graph templates, giving various conditions for both tractability and hardness. For quantifiers there exists>=1 and there exists>=2, we give a dichotomy for all graphs, namely, the problem is NP-hard if the graph contains a triangle or has girth at least 5, and is in P otherwise. We strengthen this result in the following two ways. For bipartite graphs, the problem is in P for forests and graphs of girth 4, and is Pspace-hard otherwise. For complete multipartite graphs, the problem is in L, NP-complete, or Pspace-complete. Finally, using counting quantifiers we solve the complexity of a concrete QCSP whose complexity was previously open.
-
J6
QCSP
Florent R. Madelaine and Barnaby Martin.
The complexity of positive first-order logic without equality.
ACM Trans. Comput. Log., 13(1):5, 2012.
Journal version of
C7 together with results of Barnaby Martin
on the four element case from CSL'10, now subsumed by
J9
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
L, is NP-complete, is coNP-complete or is
Pspace-complete.
-
J5
MMSNP
Florent R. Madelaine
Universal structures and the logic of forbidden patterns.
Logical Methods in Computer Science, 5(2), 2009.
Journal version of
C2 and
C3.
Forbidden Patterns Problems (FPPs) are a proper
generalisation of Constraint Satisfaction Problems
(CSPs). However, we show that when the input is
connected and belongs to a class which has low
tree-depth decomposition (e.g. structure of bounded
degree, proper minor closed class and more generally
class of bounded expansion) any FPP becomes a
CSP. This result can also be rephrased in terms of
expressiveness of the logic MMSNP, introduced by
Feder and Vardi in relation with CSPs. Our proof
generalises that of a recent paper by Nesetril and
Ossona de Mendez. Note that our result holds in the
general setting of problems over arbitrary
relational structures (not just for graphs).
-
J4
interconnection networks
Florent R. Madelaine and Iain A. Stewart.
Improved upper and lower bounds on the feedback vertex numbers of
grids and butterflies.
Discrete Mathematics, 308(18):4144-4164, 2008.
We improve upon the best known upper and lower
bounds on the sizes of minimal feedback vertex sets
in butterflies. Also, we construct new feedback
vertex sets in grids so that for a large number of
grids, the size of our feedback vertex set in the
grid matches the best known lower bound, and for all
other grids it differs from this lower bound by at
most 2.
-
J3
MMSNP
Florent R. Madelaine and Iain A. Stewart.
Constraint satisfaction, logic and forbidden patterns.
SIAM J. Comput., 37(1):132-163, 2007.
In the early nineties, Feder and Vardi attempted to
logically characterize the class of constraint
satisfaction problems, CSP, by introducing a
syntactic fragment of existential monadic
second-order logic, namely the logic
MMSNP. They proved that MMSNP is
computationally equivalent to CSP but that
CSP is strictly included in MMSNP (as
classes of problems). We introduce here a new class
of combinatorial problems, the class of forbidden
patterns problems, FPP, and show that they
correspond (modulo technical restrictions) to the
class of problems MMSNP. We introduce some
novel algebraic tools that allow us to characterize
exactly those problems that are in FPP (and so
in MMSNP) but not in CSP. Furthermore,
given a representation for a problem in FPP,
we are able to construct a normal form and,
according to a very simple criterion, so decide
whether the problem is in CSP or not (this
whole process is effective). If the problem is in
CSP then we can construct a template for this
problem, otherwise for any given candidate for the
role of template, we can build a counter-example
(again, this process is effective).
-
J2
CSP
Tomás Feder, Florent R. Madelaine, and Iain A. Stewart.
Dichotomies for classes of homomorphism problems involving unary
functions.
Theor. Comput. Sci., 314(1-2):1-43, 2004.
We study non-uniform constraint satisfaction
problems where the underlying signature contains
constant and function symbols as well as relation
symbols. Amongst our results are the following. We
establish a dichotomy result for the class of
non-uniform constraint satisfaction problems over
the signature consisting of one unary function
symbol by showing that every such problem is either
complete for L, via very restricted logical
reductions, or trivial (depending upon whether the
template function has a fixed point or not). We show
that the class of non-uniform constraint
satisfaction problems whose templates are structures
over the signature λ2 consisting of two unary
function symbols reflects the full computational
significance of the class of non-uniform constraint
satisfaction problems over relational structures. We
prove a dichotomy result for the class of
non-uniform constraint satisfaction problems where
the template is a λ2-structure with the
property that the two unary functions involved are
the reverse of one another, in that every such
problem is either solvable in polynomial-time or
NP-complete. Finally, we extend some of our
results to the situation where instances of
non-uniform constraint satisfaction problems come
equipped with lists of elements of the template
structure which restrict the set of allowable
homomorphisms.
-
J1
CSP
Florent R. Madelaine and Iain A. Stewart.
Some problems not definable using structure homomorphisms.
Ars Comb., 67, 2003.
We exhibit some problems defined in Feder and
Vardi's logic MMSNP that are not in the class CSP of
constraint satisfaction problems. Whilst some of
these problems have previously been shown to be in
MMSNP (that is, definable in MMSNP) but not in CSP,
existing proof are probabilistic in nature. We
provide explicit combinatorial constructions to
prove that these problems are not in CSP and we use
these constructions to exhibit yet more problems in
MMSNP that are not in CSP.