みなさま

1月31日(火)と2月9日(木)にJAISTで行われます、計算量・組合せ理論についての ２つセミナーをご案内致します。どうぞお気軽にお越しください。

http://www.jaist.ac.jp/is/labs/ogawa-lab/vs12.html

廣川

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - Seminars of Research Center for Software Verification, JAIST - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

== Seminar I ==

Date: 31st Jan (Tue) 13:00-17:00 (closing time is flexible) Place: JAIST IS school collaboration room 7 (5F)

1. Prof.Yijia Chen (Shanghai Jiao Tong University) "Parameterized complexity of SAT"

Many natural computational problems are NP-hard, hence they have no polynomial time algorithms assuming NP \ne P. The traditional approaches for coping with such problems are heuristic and approximation algorithms. Nevertheless, the heuristic algorithms often lack a rigorous analysis, while the approximation algorithms cannot guarantee exact solutions. Parameterized algorithms offer another approach which achieves both criteria. The key observation is that many natural problem instances come with some parameters which can be expected to be small, e.g., the size of a vertex cover, the length of a database query, and the tree width of a graph. If an exponential time algorithm has its superpolynomial behavior restricted by the parameters, it might well be efficient in practice. As an example, there is an algorithm for SAT which is exponential in the tree width tw(\alpha) of a given instance \alpha and at the same time linear in the size of \alpha. Therefore, if there is a constant upper bound on tw(\alpha), we can solve the corresponding SAT in linear time.

In this talk I will survey some major tools for designing parameterized algorithms, including bounded search tree, kernelization, tree width method, and algorithmic meta-theorems, etc, with a focus on applications to SAT. In passing, I will also discuss some corresponding lower bound results.

2. Dr. Yohji Akama (Tohoku University) "A new order theory of set systems, WQO and BQO"

A set system over a set $T$, a subfamily of the power set $P(T)$, is a topic of (extremal) combinatorics, as well as a target of an algorithm to learn in computational learning theory of languages.

A well quasi-ordering (WQO for short) is introduced by Higman and employed in algebra, combinatorics, formal language theory, and so on. A better quasi-ordering (BQO for short) is introduced by Nash-Williams and employed in infinitary combinatorics and verification of infinite-state systems.

We generalize WQOs and BQOs by using set systems, define the order type of a set system from game-theoretic viewpoint and study nondeterministic, combinatorial operations on set systems, such as monotone (continuous) image and unbounded unions of set systems. The motivating examples are the union of two colored arithmetical progressions, and the discolorization, and new useful examples are shuffle-product and shuffle-closure from formal language theory

Furthermore, we provide a neat correspondence : quasi-orderings vs finitely branching simulations, and set systems vs linear, monotone, continuous functions.

Next, we introduce a set system that has order type and corresponds to a BQO. We prove that the class of set systems corresponding to BQOs is closed by any monotone function. In (Shinohara and Arimura. ``Inductive inference of unbounded unions of pattern languages from positive data.'', Theoretical Computer Science, pp.191-209, 2000), for any set system $L$, they considered the class of arbitrary (finite) unions of members of $L$. From viewpoint of WQOs and BQOs, we characterize the set systems $L$ such that the class of arbitrary (finite) unions of members of $L$ has order type.

== Seminar II ==

Date: 9th Feb (Thu) 13:00-15:00 (closing time is flexible) Place: JAIST IS school collaboration room 7 (5F)

* Prof.Yijia Chen (Shanghai Jiao Tong University) "A Logic for PTIME and a Parameterized Halting Problem"

Whether there is a logic for polynomial time (PTIME) is the central problem in finite model theory. When formalizing this problem, Gurevich (1988), together with Blass, actually proposed a logic LFP_inv, which is a version of least fixed-point logic plus some additional invariance condition. Although they don't believe that LFP_inv captures PTIME, no proof was given. Later, in a work of Nash, Remmel, and Vianu (2005), it was shown that whether LFP_inv captures PTIME is equivalent to the parameterized complexity of a halting problem:

input: A nondeterministic Turing machine M and a natural number n in unary. parameter: |M|, i.e., the size of M question: does M accept the empty input in at most n steps?

Our recent work (2010-11) reveals that it is even equivalent to an open problem in proof complexity, i.e., whether there is a polynomial optimal proof system for the set TAUT of tautologies of propositional logic.

In this talk, I will discuss all these equivalences and their extensions to some other complexity classes beside PTIME. It turns out that Levin's optimal inverters (1973) play a central role in the proofs.

This is joint work with Joerg Flum.