Department of Computer Science & Engineering

For each $k \geq 1$, we give a famiily of unsatisfiable sets of clauses which have polynomial size ${\mbox{Res}}(k+1)$ refutations, but which require ${\mbox{Res}}(k)$ refutations of $2^{n^{\epsilon_k}}$. This improves the superpolynomial- separation between resolution and ${\mbox{Res}}(2)$ given by Bonet and Galesi to exponential. As a corollary, we obtain an exponential separation between depth 0 Frege and depth 1 Frege, improving upon the superpolynomial separation given by the weak pigeonhole principle.

Pre-2018 CSE ID: CS2002-0697

The thin plate spline (TPS) is an effective tool for modeling coordinate transformations that has been applied successfully in several computer vision applications. Unfortunately the solution requires the inversion of a p x p matrix, where p is the number of points in the data set, thus making it impractical for large scale applications. In practical applications, however, a surprisingly good approximate solution is often possible using only a small subset of corresponding points. We begin by discussing the obvious approach of using this subset to estimate a transformation that is then applied to all the points, and we show the drawbacks of this method. We then proceed to borrow a technique from the machine learning community for function approximation using radial basis functions (RBFs) and adapt it to the task at hand. Using this method, we demonstrate a significant improvement over the naive method. One drawback of this method, however, is that is does not allow for principal warp analysis, a technique for studying shape deformations introduced by Bookstein based on the eigenvectors of the p x p bending energy matrix. To address this, we describe a third approximation method based on a classic matrix completion technique that allows for principal warp analysis as a by-product. By means of experiments on real and synthetic data, we demonstrate the pros and cons of these different approximations so as to allow the reader to make an informed decision suited to his or her application.

Pre-2018 CSE ID: CS2003-0764

Simultaneous Multithreading (SMT) architectures are appearing in commercial processors, yet there is still relatively little support for sampling or determining where to simulate to achieve representative simulation results. The challenge in creating a sampling approach to SMT is determining how far to fast-forward each individual thread between samples. Determining how far to accurately fast-forward each individual thread will vary as the threads execute through different phases of execution, and between different architecture configurations. In this paper, we examine using individual program phase information to guide simulation for Simultaneous Multithreading. This is accomplished through creating what we call a Co-Phase Matrix. The co-phase matrix represents the performance and throughput of the potential combination of the phase behavior found in multiple programs when run together. The co-phase matrix is populated by collecting samples of the program's phase combinations, and is used to to guide how far to fast-forward between samples. We show for a handful of SPEC program combinations that using the co-phase matrix provides an average error rates of 2.2% while replacing most detailed simulation with fast-forwarding.

Pre-2018 CSE ID: CS2003-0771

Managing ecosystems to maintain biodiversity may be one approach to ensuring their dynamic stability, productivity, and delivery of vital services. The applicability of this approach to industrial ecosystems that harness the metabolic activities of microbes has been proposed but has never been tested at relevant scales. We used a tag-sequencing approach with bacterial small subunit rRNA (16S) genes and eukaryotic internal transcribed spacer 2 (ITS2) to measuring the taxonomic composition and diversity of bacteria and eukaryotes in an open pond managed for bioenergy production by microalgae over a year. Periods of high eukaryotic diversity were associated with high and more-stable biomass productivity. In addition, bacterial diversity and eukaryotic diversity were inversely correlated over time, possibly due to their opposite responses to temperature. The results indicate that maintaining diverse communities may be essential to engineering stable and productive bioenergy ecosystems using microorganisms.

Background

Results

Conclusions

We address the problem of synthesizing physical animations that can loop seamlessly. We formulate a variational approach by deriving a physical law in a periodic time domain. The trajectory of the animation is represented as a parametric closed curve, and the physical law corresponds to minimizing the bending energy of the curve. Compared to traditional keyframe animation approaches, our formulation is constraint-free, which allows us to apply a standard Gauss--Newton solver. We further propose a fast projection method to efficiently generate an initial guess close to the desired animation. Our method can handle a variety of physical cyclic animations, including clothes, soft bodies with collisions, and N-body systems.