^October November – 2007 ^December

Effective resizing of images should not only use geometric constraints, but consider the image content as well. We present a simple image operator called seam carving that supports content-aware image resizing for both reduction and expansion. A seam is an optimal 8-connected path of pixels on a single image from top to bottom, or left to right, where optimality is defined by an image energy function. By repeatedly carving out or inserting seams in one direction we can change the aspect ratio of an image. By applying these operators in both directions we can retarget the image to a new size. The selection and order of seams protect the content of the image, as defined by the energy function. Seam carving can also be used for image content enhancement and object removal. We support various visual saliency measures for defining the energy of an image, and can also include user input to guide the process. By storing the order of seams in an image we create multi-size images, that are able to continuously change in real time to fit a given size.

This talk is about the application of Boolean SAT solvers to the problem of determining program termination. Proving termination is all about the search for suitable ranking functions. The key idea in this work is to encode the search for particular forms of ranking functions to Boolean statements which are satisfiable if and only if such ranking functions exist. In this way, proving termination can be performed using a state-of-the-art Boolean satisfaction solver.

We have applied this approach to several variants of the so-called LPO termination problem which comes up in the context of term rewrite systems. Experimental results are unequivocal, indicating orders of magnitude speedups in comparison with previous implementations for LPO termination. Our results have had a direct impact on the design of several major termination analyzers for term rewrite systems. Moreover, there are an increasing number of new results illustrating additional applications of SAT to proving termination.

The parallel repetition theorem, proven by Raz in 1995, is a fundamental result that in addition to its philosophical appeal, plays a key role in complexity theory. The theorem studies the behavior of success probabilities of two prover games, when many copies of such a game are played in parallel. It shows that the success probability decreases exponentially in the number of repetitions, but the parameters given by the theorem do not seem tight. It is natural to ask what are the best parameters for which the theorem holds, and improving them would have complexity theoretic implications.

This talk describes an attempt to improve the parameters in a very special case of the parallel repetition theorem. Our attempt had only limited success, but it turns out that the reason we got stuck was that the following seemingly hard question from the geometry of "foams" was hidden in the special case that we were trying to solve: What is the least surface area of a cell that tiles $R^d$ by the lattice $Z^d$? Very little about this foam problem is known. It is interesting to see such a geometric question encoded inside the problem of parallel repetition in two prover games.