Author name cluster

Frédéric Olive

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

AAAI Conference 2023 Conference Paper

Complexity of Reasoning with Cardinality Minimality Conditions

Nadia Creignou
Frédéric Olive
Johannes Schmidt

Many AI-related reasoning problems are based on the problem of satisfiability of propositional formulas with some cardinality-minimality condition. While the complexity of the satisfiability problem (SAT) is well understood when considering systematically all fragments of propositional logic within Schaefer’s framework, this is not the case when such minimality condition is added. We consider the CardMinSat problem, which asks, given a formula φ and an atom x, whether x is true in some cardinality-minimal model of φ. We completely classify the computational complexity of the CardMinSat problem within Schaefer’s framework, thus paving the way for a better understanding of the tractability frontier of many AI-related reasoning problems. To this end we use advanced algebraic tools.

PDF Details DOI

CSL Conference 2012 Conference Paper

Descriptive complexity for pictures languages

Etienne Grandjean
Frédéric Olive

This paper deals with logical characterizations of picture languages of any dimension by syntactical fragments of existential second-order logic. Two classical classes of picture languages are studied: - the class of "recognizable" picture languages, i. e. projections of languages defined by local constraints (or tilings): it is known as the most robust class extending the class of regular languages to any dimension; - the class of picture languages recognized on "nondeterministic cellular automata in linear time": cellular automata are the simplest and most natural model of parallel computation and linear time is the minimal time-bounded class allowing synchronization of nondeterministic cellular automata. We uniformly generalize to any dimension the characterization by Giammarresi et al. (1996) of the class of "recognizable" picture languages in existential monadic second-order logic. We state several logical characterizations of the class of picture languages recognized in linear time on nondeterministic cellular automata. They are the first machine-independent characterizations of complexity classes of cellular automata. Our characterizations are essentially deduced from normalization results we prove for first-order and existential second-order logics over pictures. They are obtained in a general and uniform framework that allows to extend them to other "regular" structures.

Details

SAT Conference 2011 Conference Paper

Enumerating All Solutions of a Boolean CSP by Non-decreasing Weight

Nadia Creignou
Frédéric Olive
Johannes Schmidt 0001

Abstract We address the problem of enumerating all models of Boolean formulæ in order of non-decreasing weight in Schaefer’s framework. The weight of a model is the number of variables assigned to 1. Tractability in this context amounts to enumerating all models one after the other in sorted order, with polynomial delay between two successive outputs. The question of model-enumeration has already been studied in Schaefer’s framework, but without imposing a specific order. The order of non-decreasing weight changes the complexity considerably. We obtain a new dichotomous complexity classification. On the one hand, we develop new polynomial delay algorithms for Horn and 2-XOR-formulæ to enumerate the models by non-decreasing weight. On the other hand, we prove that in all other cases such a polynomial delay algorithm does not exist, unless P=NP.

Details

CSL Conference 2006 Conference Paper

First-Order Queries over One Unary Function

Arnaud Durand 0001
Frédéric Olive

Abstract This paper investigates the complexity of query problem for first-order formulas on quasi-unary signatures, that is, on vocabularies made of a single unary function and any number of monadic predicates. We first prove a form of quantifier elimination result: any query defined by a quasi-unary first-order formula can be equivalently defined, up to a suitable linear-time reduction, by a quantifier-free formula. We then strengthen this result by showing that first-order queries on quasi-unary signatures can be computed with constant delay i. e. by an algorithm that has a precomputation part whose complexity is linear in the size of the structure followed by an enumeration of all solutions (i. e. the tuples that satisfy the formula) with a constant delay (i. e. depending on the formula size only) between each solution. Among other things, this reproves (see[7]) that such queries can be computed in total time f (| φ |). (| S |+| φ ( S )|) where S is the structure, φ is the formula, φ ( S ) is the result of the query and f is some fixed function. The main method of this paper involves basic combinatorics and can be easily automatized. Also, since a forest of (colored) unranked tree is a quasi-unary structure, all our results apply immediately to queries over that later kind of structures. Finally, we investigate the special case of conjunctive queries over quasi-unary structures and show that their combined complexity is not prohibitive, even from a dynamical (enumeration) point of view.

Details

CSL Conference 1998 Conference Paper

A Conjunctive Logical Characterization of Nondeterministic Linear Time

Frédéric Olive

Abstract We denote by \(\mathcal{G}\) ( f, 0, s ) the class of formulas of the form ∃g∀ xφ, where g is a tuple of unary function symbols, χ is a first-order variable, and ϕ quantifier-free formula of signature {g, f, 0, s}. We prove the reduction of \(\mathcal{G}\) ( f, 0, s) to the subclass \(\mathcal{G}_ \wedge ^ +\) ( f, 0, s ) of formulas written without negation nor disjunction. As a corollary we obtain a new logical characterization of the class NTIME RAM (n): the problems of this class, and notably most of the natural NP-complete problems, can be considered as models of some sentence of the type ∃ g 1. .. ∃ g p. .. ∀ x ∧σ( x )= τ(x) ( g i: unary function symbols; σ, τ: compositions of such functions), that is, in some sense, of some system of functional equations.

Details

CSL Conference 1995 Conference Paper

Monadic Logical Definability of NP-Complete Problems

Etienne Grandjean
Frédéric Olive

Abstract It is well known that monadic second-order logic with linear order captures exactly regular languages. On the other hand, if addition is allowed, then J. F. Lynch has proved that existential monadic secondorder logic captures at least all the languages in NTIME(n), and then expresses some NP-complete languages (e. g. knapsack problem). It seems that most combinatorial NP-complete problems (e. g. traveling salesman, colorability of a graph) do not belong to NTIME(n). But it has been proved that they do belong to NLIN (the similar class for RAM's). In the present paper, we prove that existential monadic second-order logic with addition captures the class NLIN, so enlarging considerably the set of natural problems expressible in this logic. Moreover, we also prove that this logic still captures NLIN even if first-order part of the second-order formulas is required to be ∀ * ∃ *, so improving the recent similar result of J. F. Lynch about NTIME( n ).

Details