OpenRaiser/Intern-Atlas huggingface dataset:
Structure-Based Local Search Heuristics for Circuit-Level Boolean Satisfiability
Venue: arXiv cs.AI 2011
Year: 2011

This work focuses on improving state-of-the-art in stochastic local search (SLS) for solving Boolean satisfiability (SAT) instances arising from real-world industrial SAT application domains. The recently introduced SLS method CRSat has been shown to noticeably improve on previously suggested SLS techniques in solving such real-world instances by combining justification-based local search with limited Boolean constraint propagation on the non-clausal formula representation form of Boolean circuits. In this work, we study possibilities of further improving the performance of CRSat by exploiting circuit-level structural knowledge for developing new search heuristics for CRSat. To this end, we introduce and experimentally evaluate a variety of search heuristics, many of which are motivated by circuit-level heuristics originally developed in completely different contexts, e.g., for electronic design automation applications. To the best of our knowledge, most of the heuristics are novel in the context of SLS for SAT and, more generally, SLS for constraint satisfaction problems.
Hybrid BDI-POMDP Framework for Multiagent Teaming
Venue: arXiv cs.MA 2011
Year: 2011

Many current large-scale multiagent team implementations can be characterized as following the belief-desire-intention (BDI) paradigm, with explicit representation of team plans. Despite their promise, current BDI team approaches lack tools for quantitative performance analysis under uncertainty. Distributed partially observable Markov decision problems (POMDPs) are well suited for such analysis, but the complexity of finding optimal policies in such models is highly intractable. The key contribution of this article is a hybrid BDI-POMDP approach, where BDI team plans are exploited to improve POMDP tractability and POMDP analysis improves BDI team plan performance. Concretely, we focus on role allocation, a fundamental problem in BDI teams: which agents to allocate to the different roles in the team. The article provides three key contributions. First, we describe a role allocation technique that takes into account future uncertainties in the domain; prior work in multiagent role allocation has failed to address such uncertainties. To that end, we introduce RMTDP (Role-based Markov Team Decision Problem), a new distributed POMDP model for analysis of role allocations. Our technique gains in tractability by significantly curtailing RMTDP policy search; in particular, BDI team plans provide incomplete RMTDP policies, and the RMTDP policy search fills the gaps in such incomplete policies by searching for the best role allocation. Our second key contribution is a novel decomposition technique to further improve RMTDP policy search efficiency. Even though limited to searching role allocations, there are still combinatorially many role allocations, and evaluating each in RMTDP to identify the best is extremely difficult. Our decomposition technique exploits the structure in the BDI team plans to significantly prune the search space of role allocations. Our third key contribution is a significantly faster policy evaluation algorithm suited for our BDI-POMDP hybrid approach. Finally, we also present experimental results from two domains: mission rehearsal simulation and RoboCupRescue disaster rescue simulation.
Generalizing Boolean Satisfiability II: Theory
Venue: arXiv cs.AI 2011
Year: 2011

This is the second of three planned papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal is to define a representation in which this structure is apparent and can easily be exploited to improve computational performance. This paper presents the theoretical basis for the ideas underlying ZAP, arguing that existing ideas in this area exploit a single, recurring structure in that multiple database axioms can be obtained by operating on a single axiom using a subgroup of the group of permutations on the literals in the problem. We argue that the group structure precisely captures the general structure at which earlier approaches hinted, and give numerous examples of its use. We go on to extend the Davis-Putnam-Logemann-Loveland inference procedure to this broader setting, and show that earlier computational improvements are either subsumed or left intact by the new method. The third paper in this series discusses ZAPs implementation and presents experimental performance results.
Learning Content Selection Rules for Generating Object Descriptions in Dialogue
Venue: arXiv cs.CL 2011
Year: 2011

A fundamental requirement of any task-oriented dialogue system is the ability to generate object descriptions that refer to objects in the task domain. The subproblem of content selection for object descriptions in task-oriented dialogue has been the focus of much previous work and a large number of models have been proposed. In this paper, we use the annotated COCONUT corpus of task-oriented design dialogues to develop feature sets based on Dale and Reiters (1995) incremental model, Brennan and Clarks (1996) conceptual pact model, and Jordans (2000b) intentional influences model, and use these feature sets in a machine learning experiment to automatically learn a model of content selection for object descriptions. Since Dale and Reiters model requires a representation of discourse structure, the corpus annotations are used to derive a representation based on Grosz and Sidners (1986) theory of the intentional structure of discourse, as well as two very simple representations of discourse structure based purely on recency. We then apply the rule-induction program RIPPER to train and test the content selection component of an object description generator on a set of 393 object descriptions from the corpus. To our knowledge, this is the first reported experiment of a trainable content selection component for object description generation in dialogue. Three separate content selection models that are based on the three theoretical models, all independently achieve accuracies significantly above the majority class baseline (17%) on unseen test data, with the intentional influences model (42.4%) performing significantly better than either the incremental model (30.4%) or the conceptual pact model (28.9%). But the best performing models combine all the feature sets, achieving accuracies near 60%. Surprisingly, a simple recency-based representation of discourse structure does as well as one based on intentional structure. To our knowledge, this is also the first empirical comparison of a representation of Grosz and Sidners model of discourse structure with a simpler model for any generation task.
Efficiency versus Convergence of Boolean Kernels for On-Line Learning Algorithms
Venue: arXiv cs.LG 2011
Year: 2011

The paper studies machine learning problems where each example is described using a set of Boolean features and where hypotheses are represented by linear threshold elements. One method of increasing the expressiveness of learned hypotheses in this context is to expand the feature set to include conjunctions of basic features. This can be done explicitly or where possible by using a kernel function. Focusing on the well known Perceptron and Winnow algorithms, the paper demonstrates a tradeoff between the computational efficiency with which the algorithm can be run over the expanded feature space and the generalization ability of the corresponding learning algorithm. We first describe several kernel functions which capture either limited forms of conjunctions or all conjunctions. We show that these kernels can be used to efficiently run the Perceptron algorithm over a feature space of exponentially many conjunctions; however we also show that using such kernels, the Perceptron algorithm can provably make an exponential number of mistakes even when learning simple functions. We then consider the question of whether kernel functions can analogously be used to run the multiplicative-update Winnow algorithm over an expanded feature space of exponentially many conjunctions. Known upper bounds imply that the Winnow algorithm can learn Disjunctive Normal Form (DNF) formulae with a polynomial mistake bound in this setting. However, we prove that it is computationally hard to simulate Winnows behavior for learning DNF over such a feature set. This implies that the kernel functions which correspond to running Winnow for this problem are not efficiently computable, and that there is no general construction that can run Winnow with kernels.
Risk-Sensitive Reinforcement Learning Applied to Control under Constraints
Venue: arXiv cs.LG 2011
Year: 2011

In this paper, we consider Markov Decision Processes (MDPs) with error states. Error states are those states entering which is undesirable or dangerous. We define the risk with respect to a policy as the probability of entering such a state when the policy is pursued. We consider the problem of finding good policies whose risk is smaller than some user-specified threshold, and formalize it as a constrained MDP with two criteria. The first criterion corresponds to the value function originally given. We will show that the risk can be formulated as a second criterion function based on a cumulative return, whose definition is independent of the original value function. We present a model free, heuristic reinforcement learning algorithm that aims at finding good deterministic policies. It is based on weighting the original value function and the risk. The weight parameter is adapted in order to find a feasible solution for the constrained problem that has a good performance with respect to the value function. The algorithm was successfully applied to the control of a feed tank with stochastic inflows that lies upstream of a distillation column. This control task was originally formulated as an optimal control problem with chance constraints, and it was solved under certain assumptions on the model to obtain an optimal solution. The power of our learning algorithm is that it can be used even when some of these restrictive assumptions are relaxed.
Approximate Policy Iteration with a Policy Language Bias: Solving Relational Markov Decision Processes
Venue: arXiv cs.AI 2011
Year: 2011

We study an approach to policy selection for large relational Markov Decision Processes (MDPs). We consider a variant of approximate policy iteration (API) that replaces the usual value-function learning step with a learning step in policy space. This is advantageous in domains where good policies are easier to represent and learn than the corresponding value functions, which is often the case for the relational MDPs we are interested in. In order to apply API to such problems, we introduce a relational policy language and corresponding learner. In addition, we introduce a new bootstrapping routine for goal-based planning domains, based on random walks. Such bootstrapping is necessary for many large relational MDPs, where reward is extremely sparse, as API is ineffective in such domains when initialized with an uninformed policy. Our experiments show that the resulting system is able to find good policies for a number of classical planning domains and their stochastic variants by solving them as extremely large relational MDPs. The experiments also point to some limitations of our approach, suggesting future work.
Quantum information approach to the ultimatum game
Venue: arXiv cs.GT 2011
Year: 2011

The paper is devoted to quantization of extensive games with the use of both the Marinatto-Weber and the Eisert-Wilkens-Lewenstein concept of quantum game. We revise the current conception of quantum ultimatum game and we show why the proposal is unacceptable. To support our comment, we present the new idea of the quantum ultimatum game. Our scheme also makes a point of departure for a protocol to quantize extensive games.
Finding missing edges and communities in incomplete networks
Venue: arXiv cs.SI 2011
Year: 2011

Many algorithms have been proposed for predicting missing edges in networks, but they do not usually take account of which edges are missing. We focus on networks which have missing edges of the form that is likely to occur in real networks, and compare algorithms that find these missing edges. We also investigate the effect of this kind of missing data on community detection algorithms.
Efficiency of Biometric integration with Salt Value at an Enterprise Level and Data Centres
Venue: arXiv cs.CR 2011
Year: 2011

This chapter is going to deal with enhancing the efficiency of Biometric by integrating it with Salt Value (randomly generated value of varying length). Normally at an enterprise level or data centres, the servers are maintained with complex passwords and they are known only to the system administrators. Even after applying lot of securities at an expert level, the hackers are able to penetrate through the network and break the passwords easily. Here how the biometric can play a vital role and that too with the inclusion of Salt value can prevent the hacker from stealing the confidential data's of an organization.
A Probabilistic Framework for Discriminative Dictionary Learning
Venue: arXiv cs.CV 2011
Year: 2011

In this paper, we address the problem of discriminative dictionary learning (DDL), where sparse linear representation and classification are combined in a probabilistic framework. As such, a single discriminative dictionary and linear binary classifiers are learned jointly. By encoding sparse representation and discriminative classification models in a MAP setting, we propose a general optimization framework that allows for a data-driven tradeoff between faithful representation and accurate classification. As opposed to previous work, our learning methodology is capable of incorporating a diverse family of classification cost functions (including those used in popular boosting methods), while avoiding the need for involved optimization techniques. We show that DDL can be solved by a sequence of updates that make use of well-known and well-studied sparse coding and dictionary learning algorithms from the literature. To validate our DDL framework, we apply it to digit classification and face recognition and test it on standard benchmarks.
Optimal Index Assignment for Multiple Description Scalar Quantization
Venue: arXiv cs.IT 2011
Year: 2011

We provide a method for designing an optimal index assignment for scalar K-description coding. The method stems from a construction of translated scalar lattices, which provides a performance advantage by exploiting a so-called staggered gain. Interestingly, generation of the optimal index assignment is based on a lattice in K-1 dimensional space. The use of the K-1 dimensional lattice facilitates analytic insight into the performance and eliminates the need for a greedy optimization of the index assignment. It is shown that that the optimal index assignment is not unique. This is illustrated for the two-description case, where a periodic index assignment is selected from possible optimal assignments and described in detail. The new index assignment is applied to design of a K-description quantizer, which is found to outperform a reference K-description quantizer at high rates. The performance advantage due to the staggered gain increases with increasing redundancy among the descriptions.
Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages
Venue: arXiv cs.LO 2011
Year: 2011

Providing adequate tools to tackle the problem of inconsistent compliance rules is a critical research topic. This problem is of paramount importance to achieve automatic support for early declarative design and to support evolution of rules in contract-based or service-based systems. In this paper we investigate the problem of extracting temporal unsatisfiable cores in order to detect the inconsistent part of a specification. We extend conflict-driven SAT-solver to provide a new conflict-driven depth-first-search solver for temporal logic. We use this solver to compute LTL unsatisfiable cores without re-exploring the history of the solver.
From Contracts in Structured English to CL Specifications
Venue: arXiv cs.CL 2011
Year: 2011

In this paper we present a framework to analyze conflicts of contracts written in structured English. A contract that has manually been rewritten in a structured English is automatically translated into a formal language using the Grammatical Framework (GF). In particular we use the contract language CL as a target formal language for this translation. In our framework CL specifications could then be input into the tool CLAN to detect the presence of conflicts (whether there are contradictory obligations, permissions, and prohibitions. We also use GF to get a version in (restricted) English of CL formulae. We discuss the implementation of such a framework.
Node-Disjoint Multipath Spanners and their Relationship with Fault-Tolerant Spanners
Venue: arXiv cs.NI 2011
Year: 2011

Motivated by multipath routing, we introduce a multi-connected variant of spanners. For that purpose we introduce the $p$-multipath cost between two nodes $u$ and $v$ as the minimum weight of a collection of $p$ internally vertex-disjoint paths between $u$ and $v$. Given a weighted graph $G$, a subgraph $H$ is a $p$-multipath $s$-spanner if for all $u,v$, the $p$-multipath cost between $u$ and $v$ in $H$ is at most $s$ times the $p$-multipath cost in $G$. The $s$ factor is called the stretch. Building upon recent results on fault-tolerant spanners, we show how to build $p$-multipath spanners of constant stretch and of $\tO(n^{1+1/k})$ edges, for fixed parameters $p$ and $k$, $n$ being the number of nodes of the graph. Such spanners can be constructed by a distributed algorithm running in $O(k)$ rounds. Additionally, we give an improved construction for the case $p=k=2$. Our spanner $H$ has $O(n^{3/2})$ edges and the $p$-multipath cost in $H$ between any two node is at most twice the corresponding one in $G$ plus $O(W)$, $W$ being the maximum edge weight.
Capacity Pre-Log of SIMO Correlated Block-Fading Channels
Venue: arXiv cs.IT 2011
Year: 2011

We establish an upper bound on the noncoherent capacity pre-log of temporally correlated block-fading single-input multiple-output (SIMO) channels. The upper bound matches the lower bound recently reported in Riegler et al. (2011), and, hence, yields a complete characterization of the SIMO noncoherent capacity pre-log, provided that the channel covariance matrix satisfies a mild technical condition. This result allows one to determine the optimal number of receive antennas to be used to maximize the capacity pre-log for a given block-length and a given rank of the channel covariance matrix.
On Validating Boolean Optimizers
Venue: arXiv cs.AI 2011
Year: 2011

Boolean optimization finds a wide range of application domains, that motivated a number of different organizations of Boolean optimizers since the mid 90s. Some of the most successful approaches are based on iterative calls to an NP oracle, using either linear search, binary search or the identification of unsatisfiable sub-formulas. The increasing use of Boolean optimizers in practical settings raises the question of confidence in computed results. For example, the issue of confidence is paramount in safety critical settings. One way of increasing the confidence of the results computed by Boolean optimizers is to develop techniques for validating the results. Recent work studied the validation of Boolean optimizers based on branch-and-bound search. This paper complements existing work, and develops methods for validating Boolean optimizers that are based on iterative calls to an NP oracle. This entails implementing solutions for validating both satisfiable and unsatisfiable answers from the NP oracle. The work described in this paper can be applied to a wide range of Boolean optimizers, that find application in Pseudo-Boolean Optimization and in Maximum Satisfiability. Preliminary experimental results indicate that the impact of the proposed method in overall performance is negligible.
Solving large linear algebraic systems in the context of integrable non-abelian Laurent ODEs
Venue: arXiv cs.SC 2011
Year: 2011

The paper reports on a computer algebra program LSSS (Linear Selective Systems Solver) for solving linear algebraic systems with rational coefficients. The program is especially efficient for very large sparse systems that have a solution in which many variables take the value zero. The program is applied to the symmetry investigation of a non-abelian Laurent ODE introduced recently by M. Kontsevich. The computed symmetries confirmed that a Lax pair found for this system earlier generates all first integrals of degree at least up to 14.
A New Framework for Network Disruption
Venue: arXiv cs.SI 2011
Year: 2011

Traditional network disruption approaches focus on disconnecting or lengthening paths in the network. We present a new framework for network disruption that attempts to reroute flow through critical vertices via vertex deletion, under the assumption that this will render those vertices vulnerable to future attacks. We define the load on a critical vertex to be the number of paths in the network that must flow through the vertex. We present graph-theoretic and computational techniques to maximize this load, firstly by removing either a single vertex from the network, secondly by removing a subset of vertices.
Convolutional Network Coding Based on Matrix Power Series Representation
Venue: arXiv cs.IT 2011
Year: 2011

In this paper, convolutional network coding is formulated by means of matrix power series representation of the local encoding kernel (LEK) matrices and global encoding kernel (GEK) matrices to establish its theoretical fundamentals for practical implementations. From the encoding perspective, the GEKs of a convolutional network code (CNC) are shown to be uniquely determined by its LEK matrix $K(z)$ if $K_0$, the constant coefficient matrix of $K(z)$, is nilpotent. This will simplify the CNC design because a nilpotent $K_0$ suffices to guarantee a unique set of GEKs. Besides, the relation between coding topology and $K(z)$ is also discussed. From the decoding perspective, the main theme is to justify that the first $L+1$ terms of the GEK matrix $F(z)$ at a sink $r$ suffice to check whether the code is decodable at $r$ with delay $L$ and to start decoding if so. The concomitant decoding scheme avoids dealing with $F(z)$, which may contain infinite terms, as a whole and hence reduces the complexity of decodability check. It potentially makes CNCs applicable to wireless networks.