Florent Madelaine

Conferences

C21 FO Fatemeh Ghasemi, Julien Grange, Mamadou Moustapha Kanté, and Florent Madelaine.
Weakly-sparse and strongly flip-flat classes of graphs are almost-wide. 08/2025. Under review.

In this work we take a step towards characterising strongly flip-flat classes of graphs. Strong flip-flatness appears to be the analogue of uniform almost-wideness in the setting of dense classes of graphs. We prove that strongly flip-flat classes of graphs that are weakly sparse are indeed uniformly almost-wide.
C20 MMSNP Alexey Barsukov and Florent R. Madelaine.
[ DOI | ]

On guarded extensions of MMSNP. In Gianluca Della Vedova, Besik Dundua, Steffen Lempp, and Florin Manea, editors, Unity of Logic and Computation - 19th Conference on Computability in Europe, CiE 2023, Batumi, Georgia, July 24-28, 2023, Proceedings, volume 13967 of Lecture Notes in Computer Science, pages 202--213. Springer, 2023.

We investigate logics and classes of problems below Fagin's existential second-order logic (ESO) and above Feder and Vardi's logic for constraint satisfaction problems (CSP), the so called monotone monadic SNP without inequality (MMSNP). It is known that MMSNP has a dichotomy between P and NP-complete but the removal of any of these three restrictions imposed on SNP yields a logic that is Ptime equivalent to ESO: so by Ladner's theorem we have three stronger sibling logics that are nondichotomic above MMSNP. In this paper, we explore the area between these four logics, mostly by considering guarded extensions of MMSNP, with the ultimate goal being to obtain logics above MMSNP that exhibit such a dichotomy.
C19 Navigational Hom Laurent Beaudou, Florent Foucaud, Florent R. Madelaine, Lhouari Nourine, and Gaétan Richard.
[ doi | pdf ]

Complexity of conjunctive regular path query homomorphisms. CiE 2019

A graph database is a digraph whose arcs are labelled with symbols from a fixed alphabet. A regular graph pattern (RGP) is a digraph whose edges are labelled with regular expressions over the alphabet. RGPs model navigational queries for graph databases, more precisely, conjunctive regular path queries. A match of a navigational RGP query in the database is witnessed by a special navigational homomorphism of the RGP to the database. We study the complexity of deciding the existence of a homomorphism between two RGPs. Such homomorphisms model a strong type of containment between two navigational RGP queries. We show that this problem can be solved by an EXPTIME algorithm (while general query containment in this context is EXPSPACE-complete). We also study the problem for restricted RGPs over a unary alphabet, that arise from some applications like XPath, and prove that certain interesting cases are polynomial-time solvable.
C18 QCSP Florent Madelaine and Stéphane Secouard.
[ doi | ]

Quantified valued constraint satisfaction problem. CP 2018: 295-311.

We study the complexity of the quantified and valued extension of the constraint satisfaction problem (QVCSP) for certain classes of languages. This problem is also known as the weighted constraint satisfaction problem with min-max quantifiers [Lee et al ICTAI 2011].
The multimorphisms that preserve a language is the starting point of our analysis. We establish some situations where a QVCSP is solvable in polynomial time by formulating new algorithms or by extending the usage of collapsibility, a property well known for reducing the complexity of the quantified CSP (QCSP) from Pspace to NP. In contrast, we identify some classes of problems for which the VCSP is tractable but the QVCSP is Pspace-hard.
As a main Corollary, we derive an analogue of Shaeffer’s dichotomy between P and Pspace for QCSP on Boolean languages and Cohen et. al. dichotomy between P and NP-complete for VCSP on Boolean valued languages : we prove that the QVCSP follows a dichotomy between P and Pspace-complete.
Finally, we exhibit examples of NP-complete QVCSP for domains of size 3 and more, which suggest at best a trichotomy between P, NP-complete and Pspace-complete for the QVCSP.
C17 QCSP Florent R. Madelaine and Barnaby Martin.
[ doi ]

Consistency for counting quantifiers. MFCS 2018.

We apply the algebraic approach for Constraint Satisfaction Problems (CSPs) with counting quantifiers, developed by Bulatov and Hedayaty, for the first time to obtain classifications for computational complexity. We develop the consistency approach for expanding polymorphisms to deduce that, if H has an expanding majority polymorphism, then the corresponding CSP with counting quantifiers is tractable. We elaborate some applications of our result, in particular deriving a complexity classification for partially reflexive graphs endowed with all unary relations. For each such structure, either the corresponding CSP with counting quantifiers is in Ptime, or it is NP-hard.
C16 MMSNP Manuel Bodirsky, Florent R. Madelaine, and Antoine Mottet.
[ arXiv | http | ]

A universal-algebraic proof of the complexity dichotomy for monotone monadic SNP. LICS 2018.

The logic MMSNP is a restricted fragment of existential second-order logic which allows to express many interesting queries in graph theory and finite model theory. The logic was introduced by Feder and Vardi who showed that every MMSNP sentence is computationally equivalent to a finite-domain constraint satisfaction problem (CSP); the involved probabilistic reductions were derandomized by Kun using explicit constructions of expander structures. We present a new proof of the reduction to finite-domain CSPs which does not rely on the results of Kun. This new proof allows us to obtain a stronger statement and to verify the more general Bodirsky-Pinsker dichotomy conjecture for CSPs in MMSNP. Our approach uses the fact that every MMSNP sentence describes a finite union of CSPs for countably infinite ω-categorical structures; moreover, by a recent result of Hubička and Nešetřil, these structures can be expanded to homogeneous structures with finite relational signature and the Ramsey property. This allows us to use the universal-algebraic approach to study the computational complexity of MMSNP.
C15 QCSP Catarina Carvalho, Florent R. Madelaine, and Barnaby Martin.
[ ArXiv | doi | ]

From complexity to algebra and back: Digraph classes, collapsibility, and the PGP. LICS 2015.

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 Π₂-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.
[Martin CP'11] Barnaby Martin: QCSP on Partially Reflexive Forests. CP 2011: 546-560
[DaMM ICALP'14] Petar Dapic, Petar Markovic, Barnaby Martin: QCSP on Semicomplete Digraphs. ICALP (1) 2014.
[Chen Sicomp'08] Hubie Chen: The Complexity of Quantified Constraint Satisfaction: Collapsibility, Sink Algebras, and the Three-Element Case. SIAM J. Comput. 37(5): 1674-1701 (2008).
C14 QCSP Florent R. Madelaine and Barnaby Martin.
[ ArXiv | doi | ]

QCSP on partially reflexive cycles - the wavy line of tractability. CSR 2013

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".
C13 QCSP Florent R. Madelaine and Barnaby Martin.
[ ArXiv | doi | ]

Containment, equivalence and coreness from CSP to QCSP and beyond. CP 2012.

The constraint satisfaction problem (CSP) and its quantified extensions, whether without (QCSP) or with disjunction (QCSP_V), 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_V before initiating a preliminary study of cores for QCSP which we characterise for certain structures and which turns out to be more elusive.
C12 QCSP Florent R. Madelaine, Barnaby Martin, and Juraj Stacho.
[ ArXiv | doi | ]

Constraint satisfaction with counting quantifiers. CSR 2012.

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) "exists at least 1" and (forall) "exists at least n" (the domain being of size n) already affords the maximal possible complexity of QCSPs (which have both there exists and for all), 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 class remains outstanding.
Afterwards, we consider the generalisation of CSPs in which we augment the extant quantifier "exists at least 1" with the quantifier "exists at least j" for j <>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.
C11 interconnection networks Yonghong Xiang, Iain A. Stewart, and Florent R. Madelaine.
[ doi | pdf | ]

Node-to-node disjoint paths in k-ary n-cubes with faulty edges. ICPADS 2011.

In a k-ary n-cube with at most 2n − 2 faulty edges, and two given nodes u and v. Assuming that m the number of healthy links of u is no more than that of v, we show that there are m disjoint paths between u and v.
C10 QCSP Florent R. Madelaine and Barnaby Martin.
[ doi | pdf | ]

A tetrachotomy for positive first-order logic without equality. LICS 2011.

We classify completely the complexity of evaluating positive equality-free sentences of first-order logic over a fixed, finite structure D. This problem may be seen as a natural generalisation of the quantified constraint satisfaction problem QCSP(D). We obtain a tetrachotomy for arbitrary finite domains: each problem is either in L, is NP-complete, is co-NP-complete or is Pspace-complete. Moreover, its complexity is characterised algebraically in terms of the presence or absence of specific surjective hyper-endomorphisms; and, logically, in terms of relativisation properties with respect to positive equality-free sentences. We prove that the meta-problem, to establish for a specific D into which of the four classes the related problem lies, is NP-hard.
C9 CSP Florent Madelaine.
[ .pdf | ]

De la complexité des problèmes de contraintes. JFPC 2011.

La conjecture de la dichotomie postule qu'un problème de satisfaction de contraintes est soit facile (dans P), soit difficile (NP-complet). Cette conjecture, motivée par Feder et Vardi il y a 20 ans, reste ouverte malgré les efforts importants d'une communauté internationale regroupant des chercheurs issus d'horizons très variés.
Nous présentons ici un bref aperçu des résultats obtenus et des techniques utilisées pour étudier cette question centrale en informatique théorique afin d'illustrer cette interdisciplinarité qui mêle algèbre, combinatoire, complexité et logique.
C8 MMSNP Florent R. Madelaine.
[ doi | pdf | ]

On the containment of forbidden patterns problems. CP 2010.

Now largely subsumed by C16

Forbidden patterns problems are a generalisation of (finite) constraint satisfaction problems which are definable in Feder and Vardi’s logic MMSNP. In fact, they are examples of infinite constraint satisfaction problems with nice model theoretic properties introduced by Bodirsky. In previous work with Iain Stewart, we introduced a normal form for these forbidden patterns problems which allowed us to provide an effective characterisation of when a problem is a finite or infinite constraint satisfaction problem. One of the central concepts of this normal form is that of a recolouring. In the presence of a recolouring from a forbidden patterns problem Ω₁ to another forbidden patterns problem Ω₂ , containment of Ω₁ in Ω₂ follows. The converse does not hold in general and it remained open whether it did in the case of problems being given in our normal form. In this paper, we prove that this is indeed the case. We also show that the recolouring problem is Π₂-hard and in Σ₃.
C7 QCSP Florent R. Madelaine and Barnaby Martin.
[ doi | .pdf | ]

The complexity of positive first-order logic without equality. LICS 2009.

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.
C6 QCSP Hubie Chen, Florent R. Madelaine, and Barnaby Martin.
[ doi | .pdf | ]

Quantified constraints and containment problems. LICS 2008.

We study two containment problems related to the quantified constraint satisfaction problem (QCSP). Firstly, we give a combinatorial condition on finite structures A and B that is necessary and sufficient to render QCSP(A) a subset of QCSP(B). The required condition is the existence of a positive integer r such that there is a surjective homomorphism from the power structure A^r to B. We note that this condition is already necessary to guarantee containment of the Π₂ restriction of QCSP, that is Π₂-CSP(A) a subset of Π₂-CSP(B). Since we are able to give an effective bound on such an r, we provide a decision procedure for the model containment problem with non-deterministic double-exponential time complexity.
Secondly, we prove that the entailment problem for quantified conjunctive-positive first-order logic is decidable. That is, given two sentences phi and psi of first-order logic with no instances of negation or disjunction, 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. quantified conjunctive-positive logic plus disjunction) is undecidable.
C5 QCSP Barnaby Martin and Florent Madelaine.
[ .pdf | ]

Quantified constraints on directed graphs. London Algorithmics and Stringology 2006, Texts in Algorithmics, King's College publication, 2007. ISBN: 9781904987413.

We study the quantified H-colouring problem for directed graphs. We prove that the quantified H-colouring problem is tractable when H is a directed cycle or a semicomplete digraph with at most one cycle. We give sufficient criteria for the quantified H-colouring problem to be in NP, and thus infer NP-completeness of the quantified H-colouring problem when H is semicomplete with more than one cycle and both a source and a sink.
C4 MMSNP Barnaby Martin and Florent R. Madelaine.
[ doi | .pdf | ]

Hierarchies in fragments of monadic strict NP. CiE 2007.

We expose a strict hierarchy within monotone monadic strict NP without inequalities (MMSNP), based on the number of second-order monadic quantifiers. We do this by studying a finer strict hierarchy within a class of forbidden patterns problems (FPP), based on the number of permitted colours. Through an adaptation of a preservation theorem of Feder and Vardi, we are able to prove that this strict hierarchy also exists in monadic strict NP (MSNP). Our hierarchy results apply over a uniform signature involving a single binary relation, that is over digraphs.
C3 MMSNP Florent R. Madelaine.
[ doi | .ps | ]

Universal structures and the logic of forbidden patterns. CSL 2006.

Forbidden Patterns Problems (FPPs) are a proper generalisation of Constraint Satisfaction Problems (CSPs). However, we show that when the input belongs to a proper minor closed class, a 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).
C2 MMSNP Stefan S. Dantchev and Florent R. Madelaine.
[ doi | .ps | ]

Bounded-degree forbidden patterns problems are constraint satisfaction problems. CSR 2006.

Forbidden Pattern problem (FPP) is a proper generalisation of Constraint Satisfaction Problem ( CSP) [J3]. FPP is related to MMSNP, a logic introduced in relation with CSP by Feder and Vardi. We prove that Forbidden Pattern Problems are Constraint Satisfaction Problems when restricted to graphs of bounded degree. This result is generalisation of a result by Häggkvist and Hell who showed that F-moteness of bounded-degree graphs is a CSP (that is, for a given graph F there exists a graph H so that the class of bounded-degree graphs that do not admit a homomorphism from F is exactly the same as the class of bounded-degree graphs that are homomorphic to H). Forbidden pattern property is a strict generalisation of F-moteness (in fact of F-moteness combined with a CSP) involving both vertex- and edge-colorings of the graph F, and thus allowing to express NP-complete problems (while F-moteness is always in P). We finally extend our result to arbitrary structures (not only graphs) and prove that every problem in MMSNP, restricted to connected input of bounded degree, is in fact in CSP.
C1 QCSP Barnaby Martin and Florent R. Madelaine.
[ doi | .ps | ]

Towards a trichotomy for quantified H-coloring. CiE 2006.

Hell and Nesetril proved that the H-coloring problem is NP-complete if, and only if, H is bipartite. In this paper, we investigate the complexity of the quantified H-coloring problem (a restriction of the quantified constraint satisfaction problem to undirected graphs). We introduce this problem using a new two player coloring game. We prove that the quantified H-coloring problem is: tractable, if H is bipartite; NP-complete, if H is not bipartite and not connected; and, Pspace complete, if H is connected and has a unique cycle, which is of odd length. We conjecture that the last case extends to all non-bipartite connected graphs.

Journals

J13 QCSP Manuel Bodirsky, Marcin Kozik, Florent R. Madelaine, Barnaby Martin, and Michal Wrona.
[ ArXiv ]

Model-checking positive equality free logic on a fixed structure (direttissima). CoRR, abs/2408.13840, 2024.

work in progress

We give a new, direct proof of the tetrachotomy classification for the model-checking problem of positive equality-free logic parameterised by the model. The four complexity classes are Logspace, NP-complete, co-NP-complete and Pspace-complete. The previous proof of this result relied on notions from universal algebra and core-like structures called U-X-cores. This new proof uses only relations, and works for infinite structures also in the distinction between Logspace and NP-hard under Turing reductions. For finite domains, the membership in NP and co-NP follows from a simple argument, which breaks down already over an infinite set with a binary relation. We develop some interesting new algorithms to solve NP and co-NP membership for a variety of infinite structures. We begin with those first-order definable in (Q;=), the so-called equality languages, then move to those first-order definable in (Q;<), the so-called temporal languages. However, it is first-order expansions of the Random Graph (V,E) that provide the most interesting examples. In all of these cases, the derived classification is a tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete.
J12 MMSNP Alexey Barsukov and Florent R. Madelaine.
[ ArXiv ]

On guarded extensions of MMSNP. Logical Methods in Computer Science, 2025.

To appear. Extended version of C20

Feder and Vardi showed that the class Monotone Monadic SNP without inequality (MMSNP) has a P vs NP-complete dichotomy if and only if such a dichotomy holds for finite-domain Constraint Satisfaction Problems (CSPs). Moreover, they showed that none of the three classes obtained by removing one of the defining properties of MMSNP (monotonicity, monadicity, no inequality) has a dichotomy. The overall objective of this paper is to study the gaps between MMSNP and each of these three superclasses, where the existence of a dichotomy remains unknown. For the gap between MMSNP and Monotone SNP without inequality, we study the class Guarded Monotone SNP without inequality (GMSNP) introduced by Bienvenu, ten Cate, Lutz, and Wolter, and prove that GMSNP has a dichotomy if and only if a dichotomy holds for GMSNP problems over signatures consisting of a unique relation symbol. For the gap between MMSNP and MMSNP with inequality, we introduce a new class MMSNP with guarded inequality, that lies between MMSNP and MMSNP with inequality and that is strictly more expressive than the former and still has a dichotomy. For the gap between MMSNP and Monadic SNP without inequality, we introduce a logic that extends the class of Matrix Partitions in a similar way how MMSNP extends finite-domain CSP, and pose an open question about the existence of a dichotomy for this class. Finally, we revisit the theorem of Feder and Vardi, which claims that the class NP embeds into MMSNP with inequality. We give a detailed proof of this theorem as it ensures no dichotomy for the right-hand side class of each of the three gaps.
J11 QCSP Catarina Carvalho, Florent R. Madelaine, Barnaby Martin, and Dmitriy Zhuk.
[ ArXiv ]

The complexity of quantified constraints: collapsibility, switchability and the algebraic formulation. ACM Trans. Comput. Log., 24(1):5:1--5:26, 2023.

Build up on C15 and other papers by my co-authors.

Let A be an idempotent algebra on a finite domain. By mediating between results of Chen and Zhuk, we argue that if A satisfies the polynomially generated powers property (PGP) and B is a constraint language invariant under A (that is, in Inv(A)), then QCSP(B) is in NP. In doing this we study the special forms of PGP, switchability and collapsibility, in detail, both algebraically and logically, addressing various questions such as decidability on the way. We then prove a complexity-theoretic converse in the case of infinite constraint languages encoded in propositional logic, that if Inv(A) satisfies the exponentially generated powers property (EGP), then QCSP(Inv(A)) is co-NP-hard. Since Zhuk proved that only PGP and EGP are possible, we derive a full dichotomy for the QCSP, justifying what we term the Revised Chen Conjecture. This result becomes more significant now the original Chen Conjecture is known to be false. Switchability was introduced by Chen as a generalisation of the already-known collapsibility. For three-element domain algebras A that are switchable and omit a G-set, we prove that, for every finite subset D of Inv(A), Pol(D) is collapsible. The significance of this is that, for QCSP on finite structures (over a three-element domain), all QCSP tractability (in P) explained by switchability is already explained by collapsibility.
J10 MMSNP Manuel Bodirsky, Florent R. Madelaine, and Antoine Mottet.
[ ArXiv ]

A proof of the algebraic tractability conjecture for monotone monadic SNP. SIAM J. Comput. 50(4), 2021.

Extended version of C16

The logic MMSNP is a restricted fragment of existential second-order logic which allows to express many interesting queries in graph theory and finite model theory. The logic was introduced by Feder and Vardi who showed that every MMSNP sentence is computationally equivalent to a finite-domain constraint satisfaction problem (CSP); the involved probabilistic reductions were derandomized by Kun using explicit constructions of expander structures. We present a new proof of the reduction to finite-domain CSPs which does not rely on the results of Kun. This new proof allows us to obtain a stronger statement and to verify the more general Bodirsky-Pinsker dichotomy conjecture for CSPs in MMSNP. Our approach uses the fact that every MMSNP sentence describes a finite union of CSPs for countably infinite ω-categorical structures; moreover, by a recent result of Hubička and Nešetřil, these structures can be expanded to homogeneous structures with finite relational signature and the Ramsey property. This allows us to use the universal-algebraic approach to study the computational complexity of MMSNP.
J9 QCSP Florent R. Madelaine and Barnaby Martin.
[ ArXiv ]

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.
[ ArXiv | doi | ]

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 Π₂ 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 φ 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.
[ ArXiV | doi | .pdf | ]

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.
[ ArXiv | .pdf | ]

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
[ ArXiv | doi ]

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.
[ doi | .pdf | ]

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.
[ doi | .pdf | ]

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.
[ doi | .ps.gz | .ps | ]

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.
[ .ps | ]

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.

Other

V2 AI for Games Florent Madelaine and Malika More.
[ http ]

Un jeu pour comprendre l'apprentissage automatique. TE 46 : Les applications de l'IA à la pédagogie Collectif Tangente, Tangente Éducation, 2018.

L'informatique débranchée permet de faire comprendre le principe de l'apprentissage automatique. L'activité présentée se base sur le jeu de Nim, dont les coups gagnants sont mémorisés à l'aide de pois chiches stockés dans des boîtes de lait.
V1 AI for Games Grégory Bonnet, Gaël Lejeune, Florent Madelaine, and Antoine Widlöcher.
[ http ]

Jeu de go : l’intelligence artificielle s'impose. Prisme, 3:12, mai 2016.

4 manches à 1. Le programme informatique AlphaGo développé par l’entreprise britannique Google DeepMind a largement dominé le champion de go sud-coréen Lee Sedol, détenteur de 18 titres internationaux. Entre les 9 et 15 mars 2016, plusieurs centaines de milliers de personnes ont suivi en direct les rencontres qui, bien au-delà du jeu, ont consacré une avancée majeure dans le champ de l’intelligence artificielle. Grégory Bonnet, Gaël Lejeune, Florent Madelaine et Antoine Widlöcher, chercheurs au Groupe de recherche en informatique, image, auto- matique & instrumentation de Caen · GREYC – UMR 6072, reviennent sur cet événement au retentissement mondial.
HdR MMSNP QCSP Florent Madelaine
[ .pdf ]

Mémoire d'habilitation à diriger des recherches. Université Clermont Ferrand 2, December 2012.

Mon travail s'articule autour des problèmes de satisfaction de contraintes (CSP) et de leurs extensions comme les problèmes de contraintes quantifiés (QCSP), la question essentielle étant de comprendre leur complexité. Ceux-ci peuvent être vus comme des problèmes de model-checking pour certains fragments de la logique du premier ordre. Dans le cas des CSP, Feder et Vardi ont proposé la conjecture de la dichotomie, à savoir que chaque problème CSP est soit facile (dans P) soit difficile (NP-complet). Dans le cas des QCSP, il n'existe pas encore de conjecture mature, mais une trichotomie entre P, NP-complet et Pspace-complet est envisageable.
Mon manuscrit comporte deux parties.
Une première partie porte sur la complexité du model checking pour les fragments syntaxiques de la logique du premier ordre et présente de manière uniforme des polychotomies pour tous ces fragments sauf CSP et QCSP. Notre méthodologie utilise trois ingrédients : algébrique (correspondance de Galois pour appréhender l'expressivité d'un ensemble de relations), combinatoire (core généralisé, i.e. sous-modèle satisfaisant les même formules pour le fragment étudié) et logique (relativisation de quantificateur(s)). En particulier, nous démontrons une tétrachotomie pour le fragment positif sans égalité de la logique du premier ordre qu'on peut voir comme une extension du QCSP pour laquelle on s'autorise la disjonction.

La seconde partie porte sur des questions autour de la logique de Feder et Vardi. Cette logique est intimement liée à la classe des CSP de domaine fini: elle exhibe une dichotomie si, et seulement si, la conjecture de la dichotomie est vraie. Un problème capturé dans cette logique s'exprime en terme de motifs coloriés interdits ou encore comme un CSP de domaine infini étudiés par Bodirsky. De plus, on peut décider lorsqu'il s'agit d'un CSP fini et l'inclusion de tels problèmes. Dans le cas spécial où ces problèmes sont aussi du premier-ordre, on retrouve des questions similaires sous le nom de dualité par homomorphisme avec les travaux en combinatoire de Nesetril et. al. De tels problèmes du premier ordre apparaissent aussi en logique lorsqu'on considère les problèmes du premier ordre préservés par homomorphisme inverse (théorème de préservation de Rossman). Ces résultats de combinatoire et de logique peuvent être relevés pour s'appliquer aux problèmes de motifs interdits. En particulier, pour des classes de structures suffisamment peu denses, les problèmes de motifs interdits sont des CSP de domaine fini.
PhD MMSNP Florent R. Madelaine
[ abstract.ps | .ps.gz | .ps ]

Constraint satisfaction problems and related logic. PhD thesis, University of Leicester, March 2003.

Constraint satisfaction problems (CSP) can be modelled in terms of the existence of a homomorphism between finite structures. Feder and Vardi have attempted to characterise logically the class CSP. They introduced a fragment of existential second order logic, the logic MMSNP. They proved that MMSNP is computationally equivalent to CSP and that CSP is strictly included in MMSNP.
In this work, we introduce a new class of combinatorial problems, the so-called forbidden patterns problems (FP), that correspond exactly to the problems definable by a sentence of MMSNP. We introduce some novel algebraic tools that allow us to characterise exactly those problems that are in FP but not in CSP. Furthermore, given a representation for a problem in FP, we are able to construct a normal form, and according to a very simple criterion, we can decide whether this problem is in CSP or not. If it is then we can construct a template for this problem (that is give this problem as a problem in CSP) and, otherwise, for any given candidate for the role of template, we can build a counter-example.
This result can be seen as a generalisation of a recent and independent work by Tardif and Nesetril. We compare our proof with their proof. Their work yields a better characterisation in the restricted case of
monochrome forbidden patterns problems. However, our construction of the template (whenever possible) is superior to theirs. Their proof relies heavily on a correspondence between gap pairs and duality pairs in the category of σ-structures. We simplify and generalise their proof to Heyting algebras . We also show that the class of forbidden patterns problems can be related to such an algebra.
We showed also that FP behaves essentially like CSP with respect to complexity: we gave complete forbidden patterns problems for the class , and , that are not in CSP. We briefly review restrictions that can lead to the tractability of forbidden patterns problems.
Finally, we investigate homomorphism problems for unary algebras: we prove a dichotomy in the case of a single unary function symbol and show that the class of problems with two unary function symbols is computationally equivalent to CSP.
Thèse MMSNP Florent Madelaine.
[ abstract.ps | .ps.gz | .ps ]

Problèmes de satisfaction de contraintes: une étude logique et combinatoire. Thèse, Université de Caen, March 2003.

Les problèmes de satisfaction de contraintes (CSP) peuvent être définis en termes d'existence d'homo-morphisme entre des structures finies. Dans une tentative de caractériser logiquement CSP, Feder et Vardi ont introduit un fragment de la logique existentielle du second ordre: la logique MMSNP. Ces derniers prouvent que la classe (des problèmes définis par les formules de la logique) MMSNP est équivalente (au sens de l'existence de réductions polynomiales) à la classe CSP, mais par contre, que CSP est strictement incluse dans MMSNP.
Dans cette thèse, on introduit une classe de problèmes combinatoires, qui correspondent exactement aux problèmes définis par les formules de la logique MMSNP: les problèmes de motifs interdits (FP). On développe des outils algébriques originaux qui permettent de caractériser les problèmes de motifs interdits qui ne sont pas dans CSP. Notons que cette preuve est fortement constructive, au sens où, étant donné la représentation d'un problème de motifs interdits, on peut le mettre sous une forme normale équivalente, puis, un critère simple permet de dire si le problème appartient à CSP ou non. De plus, si c'est le cas, on construit son patron (c'est-à-dire qu'on donne le problème en tant que problème de contraintes), sinon, on construit un programme de preuve interactive; pour tout candidat au rôle de patron, ce dernier construit un contre-exemple associé.
On contraste ce résultat avec un résultat indépendant et récent, dû à Tardif et Nesetril; leur résultat donne une meilleure caractérisation dans le cas restreint que ces auteurs considèrent: le cas des problèmes de motifs interdits monochromes; par contre, notre résultat donne une meilleure construction du patron (lorsqu'un tel patron existe). Notons que leur preuve repose essentiellement sur une correspondance entre les paires duales et les paires couvrantes dans la catégorie des σ-structures. On prouve l'existence d'une telle correspondance dans le cas général d'une algèbre de Heyting (un treillis distributif muni d'un pseudo-complément, ou exponentiel). Puis, on montre que la classe des problèmes de motifs interdits est reliée à une structure d'algèbre de Heyting.
On montre aussi que FP se comporte grosso modo de la même façon que CSP en ce qui concerne la complexité: on donne des exemples de problèmes de motifs interdits, qui sont complets pour les classes de complexité , et , et qui ne sont pas dans CSP. On étudie rapidement des restrictions classiques aux problèmes de motifs interdits qui sont susceptibles de faire baisser la complexité.
Finalement, on s'intéresse au problèmes d'homomorphismes entre des algèbres (structures fonctionnelles) finies dans le cas restreint de signatures composés uniquement de symboles unaires: premièrement, on montre l'existence d'une dichotomie pour un seul symbole; et deuxiémement, on montre que la classe des problèmes à deux symboles est équivalente (au sens de l'existence de réductions polynomiales) à CSP.