10,395 Works

Tensor Computations: Applications and Optimization (Dagstuhl Seminar 20111)

Paolo Bientinesi, David Ham, Furong Huang, Paul H. J. Kelly, Christian Lengauer & Saday Sadayappan
Tensors are higher-dimensional analogs of matrices, and represent a key data abstraction for many applications in computational science and data science. In contrast to the wide availability on diverse hardware platforms of high-performance numerical libraries for matrix computations, only limited software infrastructure exists today for high-performance tensor computations. Recent research developments have resulted in the formulation of many machine learning algorithms in terms of tensor computations. Tensor computations have also emerged as fundamental building blocks...

Frontmatter, Table of Contents, Preface, Conference Organization, Author Index

Kamal Lodaya & Meena Mahajan
This proceedings volume has the papers presented at the 30th annual conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), held at the Institute of Mathematical Sciences (IMSc), Chennai, during 1518 December 2010. The conference attracted 128 submissions from 35 countries in 6 continents, most of them of very high quality. We thank the authors who submitted for making this such a competitive conference. The PC succeeded in obtaining the help of...

Minimizing Busy Time in Multiple Machine Real-time Scheduling

Rohit Khandekar, Baruch Schieber, Hadas Shachnai & Tami Tamir
We consider the following fundamental scheduling problem. The input consists of $n$ jobs to be scheduled on a set of machines of bounded capacities. Each job is associated with a release time, a due date, a processing time and demand for machine capacity. The goal is to schedule all of the jobs non-preemptively in their release-time-deadline windows, subject to machine capacity constraints, such that the total busy time of the machines is minimized. Our problem...

Determining the Winner of a Dodgson Election is Hard

Michael Fellows, Bart M. P. Jansen, Daniel Lokshtanov, Frances A. Rosamond & Saket Saurabh
Computing the Dodgson Score of a candidate in an election is a hard computational problem, which has been analyzed using classical and parameterized analysis. In this paper we resolve two open problems regarding the parameterized complexity of DODGSON SCORE. We show that DODGSON SCORE parameterized by the target score value $k$ does not have a polynomial kernel unless the polynomial hierarchy collapses to the third level; this complements a result of Fellows, Rosamond and Slinko...

Quasi-Random PCP and Hardness of 2-Catalog Segmentation

Rishi Saket
We study the problem of 2-Catalog Segmentation which is one of the several variants of segmentation problems, introduced by Kleinberg et al., that naturally arise in data mining applications. Formally, given a bipartite graph $G = (U, V, E)$ and parameter $r$, the goal is to output two subsets $V_1, V_2 subseteq V$, each of size $r$, to maximize, $sum_{u \in U} max {|E(u, V_1)|, |E(u, V_2)|},$ where $E(u, V_i)$ is the set of edges...

Beyond Hyper-Minimisation---Minimising DBAs and DPAs is NP-Complete

Sven Schewe
In this paper we study the problem of minimising deterministic automata over finite and infinite words. Deterministic finite automata are the simplest devices to recognise regular languages, and deterministic \buchi, \cobuchi, and parity automata play a similar role in the recognition of $\omega$-regular languages. While it is well known that the minimisation of deterministic finite and weak automata is cheap, the complexity of minimising deterministic \buchi\ and parity automata has remained an open challenge. We...

Computationally Sound Abstraction and Verification of Secure Multi-Party Computations

Michael Backes, Matteo Maffei & Esfandiar Mohammadi
We devise an abstraction of secure multi-party computations in the applied $\pi$-calculus. Based on this abstraction, we propose a methodology to mechanically analyze the security of cryptographic protocols employing secure multi-party computations. We exemplify the applicability of our framework by analyzing the SIMAP sugar-beet double auction protocol. We finally study the computational soundness of our abstraction, proving that the analysis of protocols expressed in the applied $\pi$-calculus and based on our abstraction provides computational security...

Graph Isomorphism is not AC^0 reducible to Group Isomorphism

Arkadev Chattopadhyay, Jacobo Torán & Fabian Wagner
We give a new upper bound for the Group and Quasigroup Isomorphism problems when the input structures are given explicitly by multiplication tables. We show that these problems can be computed by polynomial size nondeterministic circuits of unbounded fan-in with $O(\log\log n)$ depth and $O(\log^2 n)$ nondeterministic bits, where $n$ is the number of group elements. This improves the existing upper bound from \cite{Wolf 94} for the problems. In the previous upper bound the circuits...

The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

Matthew Hague & Anthony Widjaja To
We study (collapsible) higher-order pushdown systems --- theoretically robust and well-studied models of higher-order programs --- along with their natural subclass called (collapsible) higher-order basic process algebras. We provide a comprehensive analysis of the model checking complexity of a range of both branching-time and linear-time temporal logics. We obtain tight bounds on data, expression, and combined-complexity for both (collapsible) higher-order pushdown systems and (collapsible) higher-order basic process algebra. At order-$k$, results range from polynomial to...

Reasoning About Strategies

Fabio Mogavero, Aniello Murano & Moshe Y. Vardi
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between open entities and express that the system is correct no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL*, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by SL-CHP,...

On extracting computations from propositional proofs (a survey)

Pavel Pudlák
This paper describes a project that aims at showing that propositional proofs of certain tautologies in weak proof system give upper bounds on the computational complexity of functions associated with the tautologies. Such bounds can potentially be used to prove (conditional or unconditional) lower bounds on the lengths of proofs of these tautologies and show separations of some weak proof systems. The prototype are the results showing the feasible interpolation property for resolution. In order...

Algorithms for Dynamic Speed Scaling

Susanne Albers
Many modern microprocessors allow the speed/frequency to be set dynamically. The general goal is to execute a sequence of jobs on a variable-speed processor so as to minimize energy consumption. This paper surveys algorithmic results on dynamic speed scaling. We address settings where (1) jobs have strict deadlines and (2) job flow times are to be minimized.

Structural Decomposition Methods and What They are Good For

Markus Aschinger, Conrad Drescher, Georg Gottlob, Peter Jeavons & Evgenij Thorstensen
This paper reviews structural problem decomposition methods, such as tree and path decompositions. It is argued that these notions can be applied in two distinct ways: Either to show that a problem is efficiently solvable when a width parameter is fixed, or to prove that the unrestricted (or some width-parameter free) version of a problem is tractable by using a width-notion as a mathematical tool for directly solving the problem at hand. Examples are given...

Tight bounds for rumor spreading in graphs of a given conductance

George Giakkoupis
We study the connection between the rate at which a rumor spreads throughout a graph and the conductance of the graph -- a standard measure of a graph's expansion properties. We show that for any n-node graph with conductance phi, the classical PUSH-PULL algorithm distributes a rumor to all nodes of the graph in O(phi^(-1) log(n)) rounds with high probability (w.h.p.). This bound improves a recent result of Chierichetti, Lattanzi, and Panconesi [STOC 2010], and...

Vertex Cover Kernelization Revisited: Upper and Lower Bounds for a Refined Parameter

Bart M. P. Jansen & Hans L. Bodlaender
Kernelization is a concept that enables the formal mathematical analysis of data reduction through the framework of parameterized complexity. Intensive research into the Vertex Cover problem has shown that there is a preprocessing algorithm which given an instance (G,k) of Vertex Cover outputs an equivalent instance (G',k') in polynomial time with the guarantee that G' has at most 2k' vertices (and thus O((k')^2) edges) with k' <= k. Using the terminology of parameterized complexity we...

Analysis of Agglomerative Clustering

Marcel R. Ackermann, Johannes Bloemer, Daniel Kuntze & Christian Sohler
The diameter k-clustering problem is the problem of partitioning a finite subset of R^d into k subsets called clusters such that the maximum diameter of the clusters is minimized. One early clustering algorithm that computes a hierarchy of approximate solutions to this problem for all values of k is the agglomerative clustering algorithm with the complete linkage strategy. For decades this algorithm has been widely used by practitioners. However, it is not well studied theoretically....

Spectral Sparsification in the Semi-Streaming Setting

Jonathan A. Kelner & Alex Levin
Let G be a graph with n vertices and m edges. A sparsifier of G is a sparse graph on the same vertex set approximating $G$ in some natural way. It allows us to say useful things about $G$ while considering much fewer than m edges. The strongest commonly-used notion of sparsification is spectral sparsification; H is a spectral sparsifier of G if the quadratic forms induced by the Laplacians of G and H approximate...

On Isomorphism Testing of Groups with Normal Hall Subgroups

Youming Qiao, Jayalal Sarma M.N. & Bangsheng Tang
A normal Hall subgroup $N$ of a group $G$ is a normal subgroup with its order coprime with its index. Schur-Zassenhaus theorem states that every normal Hall subgroup has a complement subgroup, that is a set of coset representatives H which also forms a subgroup of G. In this paper, we present a framework to test isomorphism of groups with at least one normal Hall subgroup, when groups are given as multiplication tables. To establish...

Quantum query complexity of minor-closed graph properties

Andrew M. Childs & Robin Kothari
We study the quantum query complexity of minor-closed graph properties, which include such problems as determining whether an $n$-vertex graph is planar, is a forest, or does not contain a path of a given length. We show that most minor-closed properties -- those that cannot be characterized by a finite set of forbidden subgraphs -- have quantum query complexity Theta(n^(3/2)). To establish this, we prove an adversary lower bound using a detailed analysis of the...

Natural Inductive Theorems for Higher-Order Rewriting

Takahito Aoto, Toshiyuki Yamada & Yuki Chiba
The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of...

Anti-Unification for Unranked Terms and Hedges

Temur Kutsia, Jordi Levy & Mateu Villaret
We study anti-unification for unranked terms and hedges that may contain term and hedge variables. The anti-unification problem of two hedges ~s_1 and ~s_2 is concerned with finding their generalization, a hedge ~q such that both ~s_1 and ~s_2 are instances of ~q under some substitutions. Hedge variables help to fill in gaps in generalizations, while term variables abstract single (sub)terms with different top function symbols. First, we design a complete and minimal algorithm to...

Automated Certified Proofs with CiME3

Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons & Xavier Urbain
We present the rewriting toolkit CiME3. Amongst other original features, this version enjoys two kinds of engines: to handle and discover proofs of various properties of rewriting systems, and to generate Coq scripts from proof traces given in certification problem format in order to certify them with a skeptical proof assistant like Coq. Thus, these features open the way for using CiME3 to add automation to proofs of termination or confluence in a formal development...

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity

Georg Moser & Andreas Schnabl
We study the complexity of rewrite systems shown terminating via the dependency pair framework using processors for reduction pairs, dependency graphs, or the subterm criterion. The complexity of such systems is bounded by a multiple recursive function, provided the complexity induced by the employed base techniques is at most multiple recursive. Moreover this upper bound is tight.

Variants, Unification, Narrowing, and Symbolic Reachability in Maude 2.6

Francisco Duran, Steven Eker, Santiago Escobar, Jose Meseguer & Carolyn Talcott
This paper introduces some novel features of Maude 2.6 focusing on the variants of a term. Given an equational theory (Sigma,Ax cup E), the E,Ax-variants of a term t are understood as the set of all pairs consisting of a substitution sigma and the E,Ax-canonical form of t sigma. The equational theory (Ax cup E ) has the finite variant property if there is a finite set of most general variants. We have added support...

Revisiting Matrix Interpretations for Proving Termination of Term Rewriting

Friedrich Neurauter & Aart Middeldorp
Matrix interpretations are a powerful technique for proving termination of term rewrite systems, which is based on the well-known paradigm of interpreting terms into a domain equipped with a suitable well-founded order, such that every rewrite step causes a strict decrease. Traditionally, one uses vectors of non-negative numbers as domain, where two vectors are in the order relation if there is a strict decrease in the respective first components and a weak decrease in all...

Registration Year

  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015
  • 2014
  • 2013
  • 2012

Resource Types

  • Text
  • Software
  • Collection