Kyoto Seminar on Teoretical Computer Sceiece

以下のセミナーが特定研究「新しいパラダイムとしてのアルゴリズム工学：計算
困難問題への挑戦」の主催で開催されます．夜の懇親会もどうぞ御参加下さい．
岩間

Kyoto Seminar on Theoretical Computer Science 

Sponsored by Scientific Research Grant, Scientific Research of
Priority Areas, Ministry of Education, Science, Sports and Culture of
Japan, "Algorithm Engineering as a New Paradigm: A Challenge to Hard
Computation Problems"

July 2 (Fri), 1999

Seminar Room, 2nd Floor
Venture Business Laboratory
Kyoto University
Sakyo, Kyoto 606-01
(For location, see  www.vbl.kyoto-u.ac.jp/About/location/index-j.html)

Contact: Prof. Kazuo Iwama (075-753-YYYY, iwama＠HOGE.kyoto-u.ac.jp)

**********************
11:00-12:00  Short Proofs are Narrow -- Resolution made Simple, 
Avi Wigderson (The Hebrew University, Jerusalem, and The Institute for
Advanced Study, Princeton)

The width of a Resolution proof is defined to be the maximal number of
literals in any clause of the proof.  In this paper we relate proof
width to proof length (=size), in both general Resolution, and its
tree-like variant. The following consequences of these relations
reveal width as a crucial ``resource'' of Resolution proofs.

In one direction, the relations allow us to give simple, unified
proofs of almost all known exponential lower bounds on size of
resolution proofs, as well as several interesting new ones. They all
follow from width lower bounds, and we show how these follow from
natural expansion property of clauses of the input tautology.

In the other direction, the width-size relations naturally suggest a
simple dynamic programming procedure for automated theorem proving -
one which simply searches for small width proofs. This relation
guarantees that the running time (and thus the size of the produced
proof) is at most quasi-polynomial in the smallest tree-like
proof. The new algorithm is never much worse than any of the recursive
automated provers (such as DLL) used in practice. In contrast, we
present a family of tautologies on which it is exponentially faster.

The lower bound part of this gap is proved using a new general
connection between the pebbling number of any graph and the tree-like
proof size of a related tautology. A byproduct is an exponential gap
between the power of general and tree-like Resolution.

Joint work with Eli Ben Sasson

**********************
12:00-13:30  Lunch

**********************
13:30-14:30  Comparison of Proof Search Algorithms for Resolution 
and Polynomial Calculus,
Maria Luisa Bonet (Cataluna Polytechnic University)

This talk is concerned with the complexity of proofs and of searching
for proofs in two propositional proof system: Resolution and
Polynomial Calculus ($PC$). For the former system we show that the
recently proposed algorithm of Ben-Sasoon and Widgerson for searching
for proofs cannot give better than weakly exponential
performance. This is a consequence of showing optimality of their
general relationship refered to as size-width trade-off. We moreover
obtain the optimality of the size-width trade-off for the widely used
restrictions of resolution: Regular, Davis-Putnam, Negative, Positive
and Linear.  As for the second system, we show that the translation to
polynomials of a $CNF$ formula having short resolution proofs, cannot
be refuted in polynomial calculus with degree less than 
$\Omega(\log n)$. A consequence of this is that the simulation of 
resolution by $PC$ of \cite{cei} cannot be improved to better than 
quasipolynomial in the case we start with small resolution proofs.  
We conjecture that the simulation of Cleg-Edmonds-Impagliazzo is optimal.

**********************
14:45-15:45  Separation of the Monotone NC Hierarchy,
Ran Raz (Weizmann Institute)

We prove tight lower bounds, of up to $n^{\epsilon}$, for the
monotone depth of functions in monotone-P.
As a result we achieve the  separation of the following classes.
1) monotone-NC $\neq$ monotone-P.
2) $\forall i \geq 1$, monotone-$NC^i$ $\neq$ monotone-$NC^{i+1}$.
3) More generally:
   For any integer function $D(n)$, up to $n^{\epsilon}$ (for some
   $\epsilon > 0$), we give an explicit example of
   a monotone Boolean function, that can be computed by
   polynomial size monotone Boolean circuits of depth $D(n)$,
   but that cannot be computed by {\bf any} (fan-in 2) monotone Boolean 
   circuits of depth less than $Const \cdot D(n)$ (for some constant $Const$).

Only a separation of monotone-$NC^1$ from monotone-$NC^{2}$
was previously known.

Our argument is more general:
we define a new class of communication complexity search problems,
referred to below as DART games, and we prove a tight lower bound for the
communication complexity of every member of this class.
As a result we get lower bounds for the monotone depth of many
functions. In particular, we get the following bounds:
1) For $st$-connectivity,  we get a tight lower bound of $\Omega(\log^2n)$.
   That is, we get a new proof for Karchmer-Wigderson's theorem,
   as an immediate corollary of our general result.
2) For the $k$-clique function, with $k \leq n^{\epsilon}$,
   we get a tight lower bound of $\Omega(k \log n)$.
   Only a bound of $\Omega(k)$ was previously known.

**********************
16:00-17:00  Scheduling Dependent Jobs and Graph Multicoloring Problems,
Magnus M Halldorsson (University of Iceland and Kyoto University)

In multiprocessor systems certain resources may not be shared
concurrently by some sets of jobs.  Scheduling dependent jobs on
multiple machines is modeled by the graph multi-coloring problem,
where each node (job) is to be assigned a set of colors (time units).
Schedules (colorings) can be either non-preemptive, when vertices are
assigned contiguous sets of colors, or preemptive.

We survey recent results on multicoloring various classes of graphs.
While much work has traditionally been done on the makespan measure
(the number of colors used), much less has been done regarding to the
sum-of-completion times measure. The latter gives rise to the *sum
multicoloring* problem. 

Some of the particular results discussed include:
 * An approximation-preserving reduction of the sum multicoloring problem 
  to finding (approximately) maximum independent sets in the given graph, 
 * Exact algorithms for various multicoloring problems on trees,
 * Polynomial time approximation schemes for multicoloring problems on
   partial k-trees and planar graphs.

This is joint work with several sets of researchers, most prominently
Amotz Bar-Noy, Guy Kortsarz, and Hadas Shachnai.

**********************
18:00-  Dinner