Date: April 29, 2022
Venue: CS building, room 0.016
Research Area: C3 Combinatorial optimization, complexity, and chip design
Friday, April 29
09:30
Coffee and Tee (room 2.075)
10:45
Coffee break (room 2.075)
Abstracts
Philipp Hieronymi: A strong version of Cobham's theorem
Let k , l > 1 be two multiplicatively independent integers. A subset X of N^n is k-recognizable if the set of k-ary representations of X is recognized by some finite automaton. Cobham’s famous theorem states that a subset of the natural numbers is both k-recognizable and l-recognizable if and only if it is Presburger-definable (or equivalently: semilinear). We show the following strengthening. Let X be k-recognizable, let Y be l-recognizable such that both X and Y are not Presburger-definable. Then the first-order logical theory of (N, +, X, Y) is undecidable. This is in contrast to a well-known theorem of Büchi that the first-order logical theory of (N, +, X) is decidable. Our work strengthens and depends on earlier work of Villemaire and Bès.
The essence of Cobham's theorem is that recognizability depends strongly on the choice of the base k. Our results strengthens this: two non-Presburger definable sets that are recognizable in multiplicatively independent bases, are not only distinct, but together computationally intractable over Presburger arithmetic. This is joint work with Christian Schulz.
Stefan Rabenstein: Faster goal-oriented shortest path search for bulk and incremental detailed routing
We develop new algorithmic techniques for VLSI detailed routing. First, we improve the goal-oriented version of Dijkstra's algorithm to find shortest paths in huge incomplete grid graphs with edge costs depending on the direction and the layer, and possibly on rectangular regions. We devise estimates of the distance to the targets that offer better trade-offs between running time and quality than previously known methods, leading to an overall speed-up. Second, we combine the advantages of the two classical detailed routing approaches - global shortest path search and track assignment with local corrections - by treating input wires (such as the output of track assignment) as reservations that can be used at a discount by the respective net. We show how to implement this new approach efficiently. This is joint work with Markus Ahrens, Dorothee Henke, and Jens Vygen.