|
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
|
|
