OpenRaiser/Intern-Atlas huggingface dataset:
Distributed Storage for Intermittent Energy Sources: Control Design and Performance Limits
Venue: arXiv cs.SY 2011
Year: 2011

One of the most important challenges in the integration of renewable energy sources into the power grid lies in their `intermittent' nature. The power output of sources like wind and solar varies with time and location due to factors that cannot be controlled by the provider. Two strategies have been proposed to hedge against this variability: 1) use energy storage systems to effectively average the produced power over time; 2) exploit distributed generation to effectively average production over location. We introduce a network model to study the optimal use of storage and transmission resources in the presence of random energy sources. We propose a Linear-Quadratic based methodology to design control strategies, and we show that these strategies are asymptotically optimal for some simple network topologies. For these topologies, the dependence of optimal performance on storage and transmission capacity is explicitly quantified.
Aladdin: Augmenting Urban Environments with Local Area Linked Data-Casting
Venue: arXiv cs.SI 2011
Year: 2011

Urban environments are brimming with information sources, yet these are typically disconnected from related information on the Web. Addressing this disconnect requires an infrastructure able to disseminate information to a specific micro-location, to be consumed by interested parties. This paper proposes Aladdin, an infrastructure for highly localised broadcast of Linked Data via radio waves. When combined with data retrieved from the Web, Aladdin can enable a new generation of micro-location-aware mobile applications and services.
Bit-Blasting ACL2 Theorems
Venue: arXiv cs.LO 2011
Year: 2011

Interactive theorem proving requires a lot of human guidance. Proving a property involves (1) figuring out why it holds, then (2) coaxing the theorem prover into believing it. Both steps can take a long time. We explain how to use GL, a framework for proving finite ACL2 theorems with BDD- or SAT-based reasoning. This approach makes it unnecessary to deeply understand why a property is true, and automates the process of admitting it as a theorem. We use GL at Centaur Technology to verify execution units for x86 integer, MMX, SSE, and floating-point arithmetic.
Formal verification of a deadlock detection algorithm
Venue: arXiv cs.LO 2011
Year: 2011

Deadlock detection is a challenging issue in the analysis and design of on-chip networks. We have designed an algorithm to detect deadlocks automatically in on-chip networks with wormhole switching. The algorithm has been specified and proven correct in ACL2. To enable a top-down proof methodology, some parts of the algorithm have been left unimplemented. For these parts, the ACL2 specification contains constrained functions introduced with defun-sk. We used single-threaded objects to represent the data structures used by the algorithm. In this paper, we present details on the proof of correctness of the algorithm. The process of formal verification was crucial to get the algorithm flawless. Our ultimate objective is to have an efficient executable, and formally proven correct implementation of the algorithm running in ACL2.
Finding small separators in linear time via treewidth reduction
Venue: arXiv cs.DS 2011
Year: 2011

We present a method for reducing the treewidth of a graph while preserving all of its minimal $s-t$ separators up to a certain fixed size $k$. This technique allows us to solve $s-t$ Cut and Multicut problems with various additional restrictions (e.g., the vertices being removed from the graph form an independent set or induce a connected graph) in linear time for every fixed number $k$ of removed vertices. Our results have applications for problems that are not directly defined by separators, but the known solution methods depend on some variant of separation. for example, we can solve similarly restricted generalizations of Bipartization (delete at most $k$ vertices from $G$ to make it bipartite) in almost linear time for every fixed number $k$ of removed vertices. These results answer a number of open questions in the area of parameterized complexity. Furthermore, our technique turns out to be relevant for $(H,C,K)$- and $(H,C,\le K)$-coloring problems as well, which are cardinality constrained variants of the classical $H$-coloring problem. We make progress in the classification of the parameterized complexity of these problems by identifying new cases that can be solved in almost linear time for every fixed cardinality bound.
Studying Satellite Image Quality Based on the Fusion Techniques
Venue: arXiv cs.CV 2011
Year: 2011

Various and different methods can be used to produce high-resolution multispectral images from high-resolution panchromatic image (PAN) and low-resolution multispectral images (MS), mostly on the pixel level. However, the jury is still out on the benefits of a fused image compared to its original images. There is also a lack of measures for assessing the objective quality of the spatial resolution for the fusion methods. Therefore, an objective quality of the spatial resolution assessment for fusion images is required. So, this study attempts to develop a new qualitative assessment to evaluate the spatial quality of the pan sharpened images by many spatial quality metrics. Also, this paper deals with a comparison of various image fusion techniques based on pixel and feature fusion techniques.
Welfare and Profit Maximization with Production Costs
Venue: arXiv cs.GT 2011
Year: 2011

Combinatorial Auctions are a central problem in Algorithmic Mechanism Design: pricing and allocating goods to buyers with complex preferences in order to maximize some desired objective (e.g., social welfare, revenue, or profit). The problem has been well-studied in the case of limited supply (one copy of each item), and in the case of digital goods (the seller can produce additional copies at no cost). Yet in the case of resources---oil, labor, computing cycles, etc.---neither of these abstractions is just right: additional supplies of these resources can be found, but at increasing difficulty (marginal cost) as resources are depleted. In this work, we initiate the study of the algorithmic mechanism design problem of combinatorial pricing under increasing marginal cost. The goal is to sell these goods to buyers with unknown and arbitrary combinatorial valuation functions to maximize either the social welfare, or the seller's profit; specifically we focus on the setting of \emph{posted item prices} with buyers arriving online. We give algorithms that achieve {\em constant factor} approximations for a class of natural cost functions---linear, low-degree polynomial, logarithmic---and that give logarithmic approximations for more general increasing marginal cost functions (along with a necessary additive loss). We show that these bounds are essentially best possible for these settings.
Capacity of the Gaussian Relay Channel with Correlated Noises to Within a Constant Gap
Venue: arXiv cs.IT 2011
Year: 2011

This paper studies the relaying strategies and the approximate capacity of the classic three-node Gaussian relay channel, but where the noises at the relay and at the destination are correlated. It is shown that the capacity of such a relay channel can be achieved to within a constant gap of $\hf \log_2 3 =0.7925$ bits using a modified version of the noisy network coding strategy, where the quantization level at the relay is set in a correlation dependent way. As a corollary, this result establishes that the conventional compress-and-forward scheme also achieves to within a constant gap to the capacity. In contrast, the decode-and-forward and the single-tap amplify-and-forward relaying strategies can have an infinite gap to capacity in the regime where the noises at the relay and at the destination are highly correlated, and the gain of the relay-to-destination link goes to infinity.
Towards Holistic Scene Understanding: Feedback Enabled Cascaded Classification Models
Venue: arXiv cs.CV 2011
Year: 2011

Scene understanding includes many related sub-tasks, such as scene categorization, depth estimation, object detection, etc. Each of these sub-tasks is often notoriously hard, and state-of-the-art classifiers already exist for many of them. These classifiers operate on the same raw image and provide correlated outputs. It is desirable to have an algorithm that can capture such correlation without requiring any changes to the inner workings of any classifier. We propose Feedback Enabled Cascaded Classification Models (FE-CCM), that jointly optimizes all the sub-tasks, while requiring only a `black-box' interface to the original classifier for each sub-task. We use a two-layer cascade of classifiers, which are repeated instantiations of the original ones, with the output of the first layer fed into the second layer as input. Our training method involves a feedback step that allows later classifiers to provide earlier classifiers information about which error modes to focus on. We show that our method significantly improves performance in all the sub-tasks in the domain of scene understanding, where we consider depth estimation, scene categorization, event categorization, object detection, geometric labeling and saliency detection. Our method also improves performance in two robotic applications: an object-grasping robot and an object-finding robot.
Smart Cane: Assistive Cane for Visually-impaired People
Venue: arXiv cs.SY 2011
Year: 2011

This paper reports on a study that helps visually-impaired people to walk more confidently. The study hypothesizes that a smart cane that alerts visually-impaired people over obstacles in front could help them in walking with less accident. The aim of the paper is to address the development work of a cane that could communicate with the users through voice alert and vibration, which is named Smart Cane. T he development work involves coding and physical installation. A series of tests have been carried out on the smart cane and the results are discussed. This study found that the Smart Cane functions well as intended, in alerting users about the obstacles in front
Inducing Probabilistic Programs by Bayesian Program Merging
Venue: arXiv cs.AI 2011
Year: 2011

This report outlines an approach to learning generative models from data. We express models as probabilistic programs, which allows us to capture abstract patterns within the examples. By choosing our language for programs to be an extension of the algebraic data type of the examples, we can begin with a program that generates all and only the examples. We then introduce greater abstraction, and hence generalization, incrementally to the extent that it improves the posterior probability of the examples given the program. Motivated by previous approaches to model merging and program induction, we search for such explanatory abstractions using program transformations. We consider two types of transformation: Abstraction merges common subexpressions within a program into new functions (a form of anti-unification). Deargumentation simplifies functions by reducing the number of arguments. We demonstrate that this approach finds key patterns in the domain of nested lists, including parameterized sub-functions and stochastic recursion.
Secure Capacity Region for Erasure Broadcast Channels with Feedback
Venue: arXiv cs.IT 2011
Year: 2011

We formulate and study a cryptographic problem relevant to wireless: a sender, Alice, wants to transmit private messages to two receivers, Bob and Calvin, using unreliable wireless broadcast transmissions and short public feedback from Bob and Calvin. We ask, at what rates can we broadcast the private messages if we also provide (information-theoretic) unconditional security guarantees that Bob and Calvin do not learn each-other's message? We characterize the largest transmission rates to the two receivers, for any protocol that provides unconditional security guarantees. We design a protocol that operates at any rate-pair within the above region, uses very simple interactions and operations, and is robust to misbehaving users.
Throughput-Distortion Computation Of Generic Matrix Multiplication: Toward A Computation Channel For Digital Signal Processing Systems
Venue: arXiv cs.MS 2011
Year: 2011

The generic matrix multiply (GEMM) function is the core element of high-performance linear algebra libraries used in many computationally-demanding digital signal processing (DSP) systems. We propose an acceleration technique for GEMM based on dynamically adjusting the imprecision (distortion) of computation. Our technique employs adaptive scalar companding and rounding to input matrix blocks followed by two forms of packing in floating-point that allow for concurrent calculation of multiple results. Since the adaptive companding process controls the increase of concurrency (via packing), the increase in processing throughput (and the corresponding increase in distortion) depends on the input data statistics. To demonstrate this, we derive the optimal throughput-distortion control framework for GEMM for the broad class of zero-mean, independent identically distributed, input sources. Our approach converts matrix multiplication in programmable processors into a computation channel: when increasing the processing throughput, the output noise (error) increases due to (i) coarser quantization and (ii) computational errors caused by exceeding the machine-precision limitations. We show that, under certain distortion in the GEMM computation, the proposed framework can significantly surpass 100% of the peak performance of a given processor. The practical benefits of our proposal are shown in a face recognition system and a multi-layer perceptron system trained for metadata learning from a large music feature database.
Massively parallel computing on an organic molecular layer
Venue: arXiv cs.ET 2011
Year: 2011

Current computers operate at enormous speeds of ~10^13 bits/s, but their principle of sequential logic operation has remained unchanged since the 1950s. Though our brain is much slower on a per-neuron base (~10^3 firings/s), it is capable of remarkable decision-making based on the collective operations of millions of neurons at a time in ever-evolving neural circuitry. Here we use molecular switches to build an assembly where each molecule communicates-like neurons-with many neighbors simultaneously. The assembly's ability to reconfigure itself spontaneously for a new problem allows us to realize conventional computing constructs like logic gates and Voronoi decompositions, as well as to reproduce two natural phenomena: heat diffusion and the mutation of normal cells to cancer cells. This is a shift from the current static computing paradigm of serial bit-processing to a regime in which a large number of bits are processed in parallel in dynamically changing hardware.
From Total Assignment Enumeration to Modern SAT Solver
Venue: arXiv cs.LO 2011
Year: 2011

A new framework for presenting and analyzing the functionality of a modern DLL-based SAT solver is proposed. Our approach exploits the inherent relation between backtracking and resolution. We show how to derive the algorithm of a modern SAT solver from DLL step-by-step. We analyze the inference power of Boolean Constraint Propagation, Non-Chronological Backtracking and 1UIP-based Conflict-Directed Backjumping. Our work can serve as an introduction to a modern SAT solver functionality and as a basis for future work on the inference power of a modern SAT solver and on practical SAT solver design.
Location-aided Distributed Primary User Identification in a Cognitive Radio Scenario
Venue: arXiv cs.NI 2011
Year: 2011

We address a cognitive radio scenario, where a number of secondary users performs identification of which primary user, if any, is transmitting, in a distributed way and using limited location information. We propose two fully distributed algorithms: the first is a direct identification scheme, and in the other a distributed sub-optimal detection based on a simplified Neyman-Pearson energy detector precedes the identification scheme. Both algorithms are studied analytically in a realistic transmission scenario, and the advantage obtained by detection pre-processing is also verified via simulation. Finally, we give details of their fully distributed implementation via consensus averaging algorithms.
A Counterexample to the Generalized Linial-Nisan Conjecture
Venue: arXiv cs.CC 2011
Year: 2011

In earlier work, we gave an oracle separating the relational versions of BQP and the polynomial hierarchy, and showed that an oracle separating the decision versions would follow from what we called the Generalized Linial-Nisan (GLN) Conjecture: that "almost k-wise independent" distributions are indistinguishable from the uniform distribution by constant-depth circuits. The original Linial-Nisan Conjecture was recently proved by Braverman; we offered a $200 prize for the generalized version. In this paper, we save ourselves $200 by showing that the GLN Conjecture is false, at least for circuits of depth 3 and higher. As a byproduct, our counterexample also implies that Pi2P is not contained in P^NP relative to a random oracle with probability 1. It has been conjectured since the 1980s that PH is infinite relative to a random oracle, but the highest levels of PH previously proved separate were NP and coNP. Finally, our counterexample implies that the famous results of Linial, Mansour, and Nisan, on the structure of AC0 functions, cannot be improved in several interesting respects.
Ranked Sparse Signal Support Detection
Venue: arXiv cs.IT 2011
Year: 2011

This paper considers the problem of detecting the support (sparsity pattern) of a sparse vector from random noisy measurements. Conditional power of a component of the sparse vector is defined as the energy conditioned on the component being nonzero. Analysis of a simplified version of orthogonal matching pursuit (OMP) called sequential OMP (SequOMP) demonstrates the importance of knowledge of the rankings of conditional powers. When the simple SequOMP algorithm is applied to components in nonincreasing order of conditional power, the detrimental effect of dynamic range on thresholding performance is eliminated. Furthermore, under the most favorable conditional powers, the performance of SequOMP approaches maximum likelihood performance at high signal-to-noise ratio.
Packing, Scheduling and Covering Problems in a Game-Theoretic Perspective
Venue: arXiv cs.GT 2011
Year: 2011

Many packing, scheduling and covering problems that were previously considered by computer science literature in the context of various transportation and production problems, appear also suitable for describing and modeling various fundamental aspects in networks optimization such as routing, resource allocation, congestion control, etc. Various combinatorial problems were already studied from the game theoretic standpoint, and we attempt to complement to this body of research. Specifically, we consider the bin packing problem both in the classic and parametric versions, the job scheduling problem and the machine covering problem in various machine models. We suggest new interpretations of such problems in the context of modern networks and study these problems from a game theoretic perspective by modeling them as games, and then concerning various game theoretic concepts in these games by combining tools from game theory and the traditional combinatorial optimization. In the framework of this research we introduce and study models that were not considered before, and also improve upon previously known results.
An algebraic approach to source coding with side information using list decoding
Venue: arXiv cs.IT 2011
Year: 2011

Existing literature on source coding with side information (SCSI) mostly uses the state-of-the-art channel codes namely LDPC codes, turbo codes, and their variants and assume classical unique decoding. In this paper, we present an algebraic approach to SCSI based on the list decoding of the underlying channel codes. We show that the theoretical limit of SCSI can be achieved in the proposed list decoding based framework when the correlation between the source and side information is $q$-ary symmetric. We argue that, as opposed to channel coding, the correct sequence from the list produced by the list decoder can effectively be recovered in case of SCSI with a few CRC symbols. The CRC symbols, which allow the decoder to identify the correct sequence, incur negligible overhead for large block lengths. More importantly, these CRC symbols are not subject to noise since we are dealing with a virtual noisy channel rather than a real noisy channel. Finally, we present a guideline for designing constructive SCSI schemes for non-binary and binary sources using Reed Solomon codes and BCH codes, respectively. This guideline allows us to design a SCSI scheme for any arbitrary $q$-ary symmetric correlation without resorting to simulation.
Multicommodity Flows and Cuts in Polymatroidal Networks
Venue: arXiv cs.DS 2011
Year: 2011

We consider multicommodity flow and cut problems in {\em polymatroidal} networks where there are submodular capacity constraints on the edges incident to a node. Polymatroidal networks were introduced by Lawler and Martel and Hassin in the single-commodity setting and are closely related to the submodular flow model of Edmonds and Giles; the well-known maxflow-mincut theorem holds in this more general setting. Polymatroidal networks for the multicommodity case have not, as far as the authors are aware, been previously explored. Our work is primarily motivated by applications to information flow in wireless networks. We also consider the notion of undirected polymatroidal networks and observe that they provide a natural way to generalize flows and cuts in edge and node capacitated undirected networks. We establish poly-logarithmic flow-cut gap results in several scenarios that have been previously considered in the standard network flow models where capacities are on the edges or nodes. Our results have already found aplications in wireless network information flow and we anticipate more in the future. On the technical side our key tools are the formulation and analysis of the dual of the flow relaxations via continuous extensions of submodular functions, in particular the Lovász extension. For directed graphs we rely on a simple yet useful reduction from polymatroidal networks to standard networks. For undirected graphs we rely on the interplay between the Lovász extension of a submodular function and line embeddings with low average distortion introduced by Matousek and Rabinovich; this connection is inspired by, and generalizes, the work of Feige, Hajiaghayi and Lee on node-capacitated multicommodity flows and cuts. The applicability of embeddings to polymatroidal networks is of independent mathematical interest.
Reasoning with Very Expressive Fuzzy Description Logics
Venue: arXiv cs.AI 2011
Year: 2011

It is widely recognized today that the management of imprecision and vagueness will yield more intelligent and realistic knowledge-based applications. Description Logics (DLs) are a family of knowledge representation languages that have gained considerable attention the last decade, mainly due to their decidability and the existence of empirically high performance of reasoning algorithms. In this paper, we extend the well known fuzzy ALC DL to the fuzzy SHIN DL, which extends the fuzzy ALC DL with transitive role axioms (S), inverse roles (I), role hierarchies (H) and number restrictions (N). We illustrate why transitive role axioms are difficult to handle in the presence of fuzzy interpretations and how to handle them properly. Then we extend these results by adding role hierarchies and finally number restrictions. The main contributions of the paper are the decidability proof of the fuzzy DL languages fuzzy-SI and fuzzy-SHIN, as well as decision procedures for the knowledge base satisfiability problem of the fuzzy-SI and fuzzy-SHIN.