PROGRAM
SESSION 1
9.00-10.00
INVITED TALK Algorithmic meta-theorems
Abstract. Algorithmic meta theorems are algorithmic
results that apply to whole families of combinatorial problems,
instead of just specific problems. These families are usually
defined in terms of logic and graph theory. An archetypal
algorithmic meta theorem is Courcelle's Theorem, which states that
all graph properties definable in monadic second-order logic can be
decided in linear time on graphs of bounded tree width. More recent
examples of such meta theorems state that all first-order definable
properties of planar graphs can be decided in linear time and that
all first-order definable optimisation problems on classes of graphs
with excluded minors can be approximated in polynomial time to any
given approximation ratio
This talk will be a survey of algorithmic meta theorems and the main
techniques used to prove such theorems.
Related survey
10.00-10.30
break
SESSION 2
10.30-11.30
INVITED TALK An algebraic approach to the constraint satisfaction problem
Abstract.
The Constraint Satisfaction Problem (CSP) provides a framework for
expressing a wide class of combinatorial problems. Given an
instance of the CSP, the aim is to determine if there is a way to
assign values from a fixed domain to the variables of the instance
so that each of its constraints is satisfied. While the entire
collection of CSPs forms an NP-complete class of problems, a number
of subclasses have been shown to be tractable (i.e., to lie in P).
A major focus of research in this area is to determine the
subclasses of the CSP that are tractable. In my talk I will present
an approach to solving this problem via universal algebra that has
been developed over the past several years. I will focus on the
Dichotomy Conjecture of Feder and Vardi and the Tractability
Conjecture of Bulatov, Jeavons, and Krokhin and describe some recent
results that provide support for both of these conjectures.
Workshop presentation
11.30-12.00
Meta-finite model expansion
12.00-12.30
On canonical forms of complete problems via first-order
projections
Nerio Borges and Blai Bonet
(Simón Bolívar University)
Abstract.
The class of problems complete for NP via first-order reductions is
known to be characterized by existential second-order sentences of a
fixed form. All such sentences are built around the so-called
generalized IS-form of the sentence that defines
Independent-Set. This result can also be understood as that every
sentence that defines a NP-complete problem P can be decomposed in
two disjuncts such that the first one characterizes a fragment of P
as hard as Independent-Set and the second the rest of P. That is, a
decomposition that divides every such sentence into a quotient and
residue modulo Independent-Set.
In this paper, we show that this result can be generalized over a
wide collection of complexity classes, including the so-called nice
classes. Moreover, we show that such decomposition can be done for
any complete problem with respect to the given class, and that two
such decompositions are non-equivalent in general. Interestingly,
our results are based on simple and well-known properties of
first-order reductions.ow that this result can be generalized over a
wide collection of complexity classes, including the so-called nice
classes. Moreover, we show that such decomposition can be done for
any complete problem with respect to the given class, and that two
such decompositions are non-equivalent in general. Interestingly,
our results are based on simple and well-known properties of
first-order reductions.
Full paper
12.30-14.00
lunch
SESSION 3
14.00-15.00
INVITED TALKExpressive power of tree logics
Abstract.
An algebraic approach to logics for finite trees. Almost any
reasonable logic over finite trees can be compiled into a finite
automaton. Examples include: XPath, monadic second-order logic (and
therefore also first-order logic), chain logic, CTL, PDL, and other
temporal logics. Furthermore, in most cases, the converse
translation fails. For instance, in the previous list, only monadic
second-order logic is capable of simulating any finite
automaton. This motivates the following question: for a given logic
(say first-order logic), describe the type of automata whose
recognized languages can be defined in this logic. We would like
this description to be effective, i.e. we would like to have an
algorithm, which answers if language recognized by the input
automaton can be defined in the logic. This type of problem is
notoriously difficult, and few results are know (the case of
first-order logic is still open). I would present an algebraic
approach to this problem, which tries to imitate semigroups theory
for words.
Workshop presentation
15.00-15.30
Order-invariant MSO is stronger than counting MSO
Abstract.
We compare the expressiveness of two extensions of monadic
second-order logic (MSO) over the class of finite structures. The
first, counting monadic second-order logic (CMSO), extends MSO with
first-order modulo-counting quantifiers, allowing the expression of
queries like ``the number of elements in the structure is
even''. The second extension allows the use of an additional binary
predicate, not contained in the signature of the queried structure,
that must be interpreted as an arbitrary linear order on its
universe, obtaining order-invariant MSO.
While it is straightforward that every CMSO formula can be
translated into an equivalent order-invariant MSO formula, the
converse had not yet been settled. Courcelle showed that for
restricted classes of structures both order-invariant MSO and CMSO
are equally expressive, but conjectured that, in general,
order-invariant MSO is stronger than CMSO. We affirm this conjecture
by presenting a class of structures that is order-invariantly
definable in MSO but not definable in CMSO.
Full paper
15.30-16.00
break
SESSION 4
16.00-17.00
INVITED TALK Resolution proof systems and clause learning SAT algorithms
Abstract.
A family of propositional resolution proof systems is
defined whose complexity — in terms of proof length
— lies
between regular and unrestricted (dag-like)
resolution. These proof systems are strongly related to
various forms of DLL jalgorithms with clause learning, which
are the basis of most contemporary SAT solvers. Finally, a
lower bound is shown for proofs of the pigeonhole principle
in a proof system that corresponds to DLL with learning of
clauses of bounded width.
Workshop presentation
17.00-17.30
Resource control of object-oriented programs
Abstract.
A sup-interpretation is a tool which provides an upper bound on the
size of a value computed by some symbol of a
program. Sup-interpretations have shown their interest to deal with
the complexity of first order functional programs. For instance,
they allow to characterize all the functions bitwise computable in
Alogtime. This paper is an attempt to adapt the framework of
sup-interpretations to a fragment of oriented-object programs,
including distinct encodings of numbers through the use of
constructor symbols, loop and while constructs and non recursive
methods with side effects. We give a criterion, called brotherly
criterion, which ensures that each brotherly program computes
objects whose size is polynomially bounded by the inputs sizes.
Full paper
17.30-18.00
Improvements on and optimality of a recent method of certifying
polynomial running time and linear/polynomial space