Stanford Theory Lunch Speaker List
Fall 2005-2006

Thursdays, 12:15pm, in the Theory Lounge (wing 4B in the Gates Computer Science building)

                Schedule 
Oct 6 Don Knuth
Shellable Boolean Functions
Oct 13 Aaron Bradley
What's Decidable About Arrays?
Oct 20 Man-Cho (Anthony) So
A Semidefinite Programming Approach to Tensegrity Theory
Oct 27 Mukund Sundararajan
Mechanism design for the rich philanthropist, the poor mother and everyone in between
Nov 3 Ho-Lin Chen
DNA Self-Assembly
Nov 10 Sergei Vassilvitskii
On the Worst-Case Complexity of the k-Means Method
Nov 17 Dominic Hughes
Proofs Without Syntax
Dec 1 Zoe Abrams
TBA
Dec 8 Cesar Sanchez
TBA

 


             Abstracts
Shellable Boolean Functions

Don Knuth

Don Knuth's talk explains a concept that will be part of Volume 4 of The Art of Computer Programming: the shelling of a boolean function. For those of you who would like to take a look, you can find links to the pre-fascicles that will be part of Volume 4 on the Don Knuth's home page news, at:

http://www-cs-faculty.stanford.edu/~knuth/news.html

In particular, the pre-fascicle on Boolean basics which includes references to the topic of tomorrow's talk can be currently downloaded from:

http://www-cs-faculty.stanford.edu/~knuth/fasc0b.ps.gz

 

What's Decidable About Arrays?

Aaron Bradley

Work on decision procedures for arrays has focused on quantifier-free fragments of array theories. For example, [Stump, Barrett, Dill & Levitt 2001] provide and prove the correctness of a decision procedure for satisfiability in the quantifier-free fragment of an extensional theory of arrays. Extensionality means that two arrays are equal iff they are element-wise equal. Decision procedures for arrays and other common theories provide the backbone of widely used verification techniques.

We study a parameterized theory of arrays in which indices are integers, as in programming languages, and in which elements are interpreted in some parameter theory. We provide and prove the correctness of a decision procedure for the "array property" fragment of the theory, which includes formulae with one quantifier alternation (with some syntactic restrictions). We also prove that for almost all extensions to the fragment, satisfiability is no longer decidable; decidability remains open for one extension. The "array property" fragment is sufficiently expressive to encode equality between (sub)arrays, properties that hold for every (or some) element of a (sub)array, and even global properties such as that a (sub)array is sorted or partitioned.

 

A Semidefinite Programming Approach to Tensegrity Theory

Man-Cho Anthony So

A tensegrity is, roughly speaking, a graph where each edge is labelled as either a bar, a cable or a strut, and each vertex is labelled as either pinned or unpinned. Each bar is given a fixed length, and each cable (resp. strut) is given an upper (resp. lower) bound on its length. The study of tensegrities is motivated by the study of stability in physical structures, and many interesting properties have been established before using non-constructive techniques. In this talk we will show that some of these properties can be established using semidefinite programming (SDP) theory, and in some cases one can even extract more information from the SDP proof than from the non-constructive proofs. If time permits, we will also discuss some appplications, e.g. the sensor network localization problem.

This is joint work with Yinyu Ye.

 

Mechanism design for the rich philanthropist, the poor mother and everyone in between

Mukund Sundararajan

We focus our attention on mechanism design for a situation where a service is to be provided to a set of agents. Agents bid how much they supposedly value the service and the service provider decides which set of agents to provide service to, and how much to charge them. Two (very social) goals that a mechanism designer may have are to achieve are efficiency and budget balance. Efficiency is defined as the difference between the total valuation of agents served and the cost of serving them, which we want to maximize( like a rich philanthropist - no reference to payments). Budget balance refers to the fact that the service provider would like to recover the cost of providing service, and while doing so, be as efficient as possible (like a poor mother and her children). It is well known fact that it is hard to simultaneously achieve both objectives- achieve perfect cost recovery while being optimally efficient.

For situations where the service provider incurs a cost submodular on the set of agents for providing service , we quantify the tension between the two objectives and show that it is possible to smoothly trade one objective for the other. In the process, we demonstrate an application of potential function style arguments.

This is joint work with Tim Roughgarden.

 

DNA Self-Assembly

Ho-Lin Chen

Self-assembly is the ubiquitous process by which objects autonomously assemble into complexes. DNA self-assembly is emerging as a key paradigm for nano-technology, nano-computation, and several related disciplines. In nature, DNA self-assembly is often equipped with explicit mechanisms for both error prevention and error correction. For artificial self-assembly, these problems are even more important since we are interested in assembling large systems with great precision.

In this talk, we will first demonstrate some recent progress on DNA self-assembly and show some issues on these achievements. Then we will present an error correction scheme on DNA self-assembly called snaked proofreading tiles and explain the basic ideas about why this system works in practice. We will also demonstrate some preliminary experimental data showing that this kind of combinatorial tile system can really change the dynamic behavior of the self-assembly process.

This is joint work with Ashish Goel, Rebecca Schulman and Erik Winfree.

 

On the Worst-Case Complexity of the k-Means Method

Sergei Vassilvitskii

The k-means method is an old but popular clustering algorithm known for its speed and simplicity. Until recently, however, no meaningful theoretical bounds were known on its running time. In this work, we demonstrate that the worst-case running time of k-means is superpolynomial by improving the best known lower bound from $\Omega(n)$ iterations to $2^{\Omega(\sqrt{n})}$. To complement this lower bound, we show a smoothed-analysis type polynomial time upper bound for k-means.

This is joint work with David Arthur

 

Proofs Without Syntax

Dominic Hughes

"Mathematicians care no more for logic than logicians for mathematics."
                                                            Augustus De Morgan, 1868

Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract mathematical formulation of propositional logic in which proofs are combinatorial (graph-theoretic), rather than syntactic. The paper defines a *combinatorial proof* of a proposition A as a graph homomorphism h : G -> G(A), where G(A) is a graph associated with A, and G is a colored graph. The main theorem is soundness and completeness: A is true iff it has a combinatorial proof. Combinatorial proofs are polynomial-time checkable, and provide a possible avenue towards NP=?=coNP.

http://boole.stanford.edu/~dominic/papers/pws

To appear in Annals of Mathematics.

 

TBA

 


    (archive of past announcements)