OpenRaiser/Intern-Atlas huggingface dataset:
A New Lower Bound on the Maximum Number of Satisfied Clauses in Max-SAT and its Algorithmic Applications
Venue: arXiv cs.DS 2011
Year: 2011

A pair of unit clauses is called conflicting if it is of the form $(x)$, $(\bar{x})$. A CNF formula is unit-conflict free (UCF) if it contains no pair of conflicting unit clauses. Lieberherr and Specker (J. ACM 28, 1981) showed that for each UCF CNF formula with $m$ clauses we can simultaneously satisfy at least $\pp m$ clauses, where $\pp =(\sqrt{5}-1)/2$. We improve the Lieberherr-Specker bound by showing that for each UCF CNF formula $F$ with $m$ clauses we can find, in polynomial time, a subformula $F'$ with $m'$ clauses such that we can simultaneously satisfy at least $\pp m+(1-\pp)m'+(2-3\pp)n"/2$ clauses (in $F$), where $n"$ is the number of variables in $F$ which are not in $F'$. We consider two parameterized versions of MAX-SAT, where the parameter is the number of satisfied clauses above the bounds $m/2$ and $m(\sqrt{5}-1)/2$. The former bound is tight for general formulas, and the later is tight for UCF formulas. Mahajan and Raman (J. Algorithms 31, 1999) showed that every instance of the first parameterized problem can be transformed, in polynomial time, into an equivalent one with at most $6k+3$ variables and $10k$ clauses. We improve this to $4k$ variables and $(2\sqrt{5}+4)k$ clauses. Mahajan and Raman conjectured that the second parameterized problem is fixed-parameter tractable (FPT). We show that the problem is indeed FPT by describing a polynomial-time algorithm that transforms any problem instance into an equivalent one with at most $(7+3\sqrt{5})k$ variables. Our results are obtained using our improvement of the Lieberherr-Specker bound above.
All Ternary Permutation Constraint Satisfaction Problems Parameterized Above Average Have Kernels with Quadratic Numbers of Variables
Venue: arXiv cs.DS 2011
Year: 2011

A ternary Permutation-CSP is specified by a subset $Π$ of the symmetric group $\mathcal S_3$. An instance of such a problem consists of a set of variables $V$ and a multiset of constraints, which are ordered triples of distinct variables of $V.$ The objective is to find a linear ordering $α$ of $V$ that maximizes the number of triples whose ordering (under $α$) follows a permutation in $Π$. We prove that all ternary Permutation-CSPs parameterized above average have kernels with quadratic numbers of variables.
Dynamic Policy Programming
Venue: arXiv cs.LG 2011
Year: 2011

In this paper, we propose a novel policy iteration method, called dynamic policy programming (DPP), to estimate the optimal policy in the infinite-horizon Markov decision processes. We prove the finite-iteration and asymptotic l\infty-norm performance-loss bounds for DPP in the presence of approximation/estimation error. The bounds are expressed in terms of the l\infty-norm of the average accumulated error as opposed to the l\infty-norm of the error in the case of the standard approximate value iteration (AVI) and the approximate policy iteration (API). This suggests that DPP can achieve a better performance than AVI and API since it averages out the simulation noise caused by Monte-Carlo sampling throughout the learning process. We examine this theoretical results numerically by com- paring the performance of the approximate variants of DPP with existing reinforcement learning (RL) methods on different problem domains. Our results show that, in all cases, DPP-based algorithms outperform other RL methods by a wide margin.
Subset feedback vertex set is fixed parameter tractable
Venue: arXiv cs.DS 2011
Year: 2011

The classical Feedback Vertex Set problem asks, for a given undirected graph G and an integer k, to find a set of at most k vertices that hits all the cycles in the graph G. Feedback Vertex Set has attracted a large amount of research in the parameterized setting, and subsequent kernelization and fixed-parameter algorithms have been a rich source of ideas in the field. In this paper we consider a more general and difficult version of the problem, named Subset Feedback Vertex Set (SUBSET-FVS in short) where an instance comes additionally with a set S ? V of vertices, and we ask for a set of at most k vertices that hits all simple cycles passing through S. Because of its applications in circuit testing and genetic linkage analysis SUBSET-FVS was studied from the approximation algorithms perspective by Even et al. [SICOMP'00, SIDMA'00]. The question whether the SUBSET-FVS problem is fixed-parameter tractable was posed independently by Kawarabayashi and Saurabh in 2009. We answer this question affirmatively. We begin by showing that this problem is fixed-parameter tractable when parametrized by |S|. Next we present an algorithm which reduces the given instance to 2^k n^O(1) instances with the size of S bounded by O(k^3), using kernelization techniques such as the 2-Expansion Lemma, Menger's theorem and Gallai's theorem. These two facts allow us to give a 2^O(k log k) n^O(1) time algorithm solving the Subset Feedback Vertex Set problem, proving that it is indeed fixed-parameter tractable.
An Upper Bound on Multi-hop Transmission Capacity with Dynamic Routing Selection
Venue: arXiv cs.IT 2011
Year: 2011

This paper develops upper bounds on the end-to-end transmission capacity of multi-hop wireless networks. Potential source-destination paths are dynamically selected from a pool of randomly located relays, from which a closed-form lower bound on the outage probability is derived in terms of the expected number of potential paths. This is in turn used to provide an upper bound on the number of successful transmissions that can occur per unit area, which is known as the transmission capacity. The upper bound results from assuming independence among the potential paths, and can be viewed as the maximum diversity case. A useful aspect of the upper bound is its simple form for an arbitrary-sized network, which allows insights into how the number of hops and other network parameters affect spatial throughput in the non-asymptotic regime. The outage probability analysis is then extended to account for retransmissions with a maximum number of allowed attempts. In contrast to prevailing wisdom, we show that predetermined routing (such as nearest-neighbor) is suboptimal, since more hops are not useful once the network is interference-limited. Our results also make clear that randomness in the location of relay sets and dynamically varying channel states is helpful in obtaining higher aggregate throughput, and that dynamic route selection should be used to exploit path diversity.
Normal Factor Graphs and Holographic Transformations
Venue: arXiv cs.IT 2011
Year: 2011

This paper stands at the intersection of two distinct lines of research. One line is "holographic algorithms," a powerful approach introduced by Valiant for solving various counting problems in computer science; the other is "normal factor graphs," an elegant framework proposed by Forney for representing codes defined on graphs. We introduce the notion of holographic transformations for normal factor graphs, and establish a very general theorem, called the generalized Holant theorem, which relates a normal factor graph to its holographic transformation. We show that the generalized Holant theorem on the one hand underlies the principle of holographic algorithms, and on the other hand reduces to a general duality theorem for normal factor graphs, a special case of which was first proved by Forney. In the course of our development, we formalize a new semantics for normal factor graphs, which highlights various linear algebraic properties that potentially enable the use of normal factor graphs as a linear algebraic tool.
Verification of Object-Oriented Programs: a Transformational Approach
Venue: arXiv cs.LO 2011
Year: 2011

We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation suggests natural proofs rules and its correctness helps us to establish soundness and relative completeness of the proposed proof system. One of the difficulties is how to properly deal in the assertion language with the instance variables and aliasing. The discussed programming language supports arrays, instance variables, failures and recursive methods with parameters.
Two-agent Nash implementation: A new result
Venue: arXiv cs.GT 2011
Year: 2011

[J. Moore and R. Repullo, \emph{Econometrica} \textbf{58} (1990) 1083-1099] and [B. Dutta and A. Sen, \emph{Rev. Econom. Stud.} \textbf{58} (1991) 121-128] are two important papers on two-agent Nash implementation. Recently, [H. Wu, Quantum mechanism helps agents combat "bad" social choice rules. \emph{International Journal of Quantum Information}, 2010 (accepted). abs/1002.4294 ] broke through traditional results on Nash implementation with three or more agents. In this paper, we will investigate two-agent Nash implementation by virtue of Wu's quantum mechanism. The main result is: A two-agent social choice rule that satisfies Condition $\mu2$ will no longer be Nash implementable if an additional Condition $λ'$ is satisfied. Moreover, according to a classical two-agent algorithm, this result holds not only in the quantum world, but also in the macro world.
LSMR: An iterative algorithm for sparse least-squares problems
Venue: arXiv cs.MS 2011
Year: 2011

An iterative method LSMR is presented for solving linear systems $Ax=b$ and least-squares problem $\min \norm{Ax-b}_2$, with $A$ being sparse or a fast linear operator. LSMR is based on the Golub-Kahan bidiagonalization process. It is analytically equivalent to the MINRES method applied to the normal equation $A\T Ax = A\T b$, so that the quantities $\norm{A\T r_k}$ are monotonically decreasing (where $r_k = b - Ax_k$ is the residual for the current iterate $x_k$). In practice we observe that $\norm{r_k}$ also decreases monotonically. Compared to LSQR, for which only $\norm{r_k}$ is monotonic, it is safer to terminate LSMR early. Improvements for the new iterative method in the presence of extra available memory are also explored.
Space-time block codes from nonassociative division algebras
Venue: arXiv cs.IT 2011
Year: 2011

Associative division algebras are a rich source of fully diverse space-time block codes (STBCs). In this paper the systematic construction of fully diverse STBCs from nonassociative algebras is discussed. As examples, families of fully diverse $2\times 2$, $2\times 4$ multiblock and $4\x 4$ STBCs are designed, employing nonassociative quaternion division algebras.
Blind Spectrum Sensing in Cognitive Radio over Fading Channels and Frequency Offsets
Venue: arXiv cs.IT 2011
Year: 2011

This paper deals with the challenging problem of spectrum sensing in cognitive radio. We consider a stochastic system model where the the Primary User (PU) transmits a periodic signal over fading channels. The effect of frequency offsets due to oscillator mismatch, and Doppler offset is studied. We show that for this case the Likelihood Ratio Test (LRT) cannot be evaluated poitnwise. We present a novel approach to approximate the marginilisation of the frequency offset using a single point estimate. This is obtained via a low complexity Constrained Adaptive Notch Filter (CANF) to estimate the frequency offset. Performance is evaluated via numerical simulations and it is shown that the proposed spectrum sensing scheme can achieve the same performance as the near-optimal scheme, that is based on a bank of matched filters, using only a fraction of the complexity required.
Parikh's Theorem: A simple and direct automaton construction
Venue: arXiv cs.FL 2011
Year: 2011

Parikh's theorem states that the Parikh image of a context-free language is semilinear or, equivalently, that every context-free language has the same Parikh image as some regular language. We present a very simple construction that, given a context-free grammar, produces a finite automaton recognizing such a regular language.
The Complexity of the Homotopy Method, Equilibrium Selection, and Lemke-Howson Solutions
Venue: arXiv cs.GT 2011
Year: 2011

We show that the widely used homotopy method for solving fixpoint problems, as well as the Harsanyi-Selten equilibrium selection process for games, are PSPACE-complete to implement. Extending our result for the Harsanyi-Selten process, we show that several other homotopy-based algorithms for finding equilibria of games are also PSPACE-complete to implement. A further application of our techniques yields the result that it is PSPACE-complete to compute any of the equilibria that could be found via the classical Lemke-Howson algorithm, a complexity-theoretic strengthening of the result in [Savani and von Stengel]. These results show that our techniques can be widely applied and suggest that the PSPACE-completeness of implementing homotopy methods is a general principle.
Separating the basic logics of the basic recurrences
Venue: arXiv cs.LO 2011
Year: 2011

This paper shows that, even at the most basic level, the parallel, countable branching and uncountable branching recurrences of Computability Logic (see http://www.cis.upenn.edu/~giorgi/cl.html) validate different principles.
Minimisation of Deterministic Parity and Buchi Automata and Relative Minimisation of Deterministic Finite Automata
Venue: arXiv cs.FL 2011
Year: 2011

In this report 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, Co-Buchi, and parity automata play a similar role in the recognition of ω-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 establish the NP-completeness of these problems. A second contribution of this report is the introduction of relaxed minimisation of deterministic finite automata. Like hyper-minimisation, relaxed minimisation allows for some changes in the language of the automaton: We seek a smallest automaton that, when used as a monitor, provides a wrong answer only a bounded number of times in any run of a system. We argue that minimisation of finite automata, hyper-minimisation, relaxed minimisation, and the minimisation of deterministic Buchi (or Co-Buchi) automata are operations of increasing reduction power, as the respective equivalence relations on automata become coarser from left to right. When we allow for minor changes in the language, relaxed minimisation can therefore be considered as a more powerful minimisation technique than hyper-minimisation from the perspective of finite automata. From the perspective of Buchi and Co-Buchi automata, we gain a cheap algorithm for state-space reduction that also turns out to be beneficial for further heuristic or exhaustive state-space reductions put on top of it.
Optimal Pricing in Social Networks with Incomplete Information
Venue: arXiv cs.GT 2011
Year: 2011

In revenue maximization of selling a digital product in a social network, the utility of an agent is often considered to have two parts: a private valuation, and linearly additive influences from other agents. We study the incomplete information case where agents know a common distribution about others' private valuations, and make decisions simultaneously. The "rational behavior" of agents in this case is captured by the well-known Bayesian Nash equilibrium. Two challenging questions arise: how to compute an equilibrium and how to optimize a pricing strategy accordingly to maximize the revenue assuming agents follow the equilibrium? In this paper, we mainly focus on the natural model where the private valuation of each agent is sampled from a uniform distribution, which turns out to be already challenging. Our main result is a polynomial-time algorithm that can exactly compute the equilibrium and the optimal price, when pairwise influences are non-negative. If negative influences are allowed, computing any equilibrium even approximately is PPAD-hard. Our algorithm can also be used to design an FPTAS for optimizing discriminative price profile.
Affine equivalence of cubic homogeneous rotation symmetric Boolean functions
Venue: arXiv cs.IT 2011
Year: 2011

Homogeneous rotation symmetric Boolean functions have been extensively studied in recent years because of their applications in cryptography. Little is known about the basic question of when two such functions are affine equivalent. The simplest case of quadratic rotation symmetric functions which are generated by cyclic permutations of the variables in a single monomial was only settled in 2009. This paper studies the much more complicated cubic case for such functions. A new concept of \emph{patterns} is introduced, by means of which the structure of the smallest group G_n, whose action on the set of all such cubic functions in $n$ variables gives the affine equivalence classes for these functions under permutation of the variables, is determined. We conjecture that the equivalence classes are the same if all nonsingular affine transformations, not just permutations, are allowed. This conjecture is verified if n < 22. Our method gives much more information about the equivalence classes; for example, in this paper we give a complete description of the equivalence classes when n is a prime or a power of 3.
Multi-Level Languages are Generalized Arrows
Venue: arXiv cs.PL 2011
Year: 2011

Multi-level languages and Arrows both facilitate metaprogramming, the act of writing a program which generates a program. The arr function required of all Arrows turns arbitrary host language expressions into guest language expressions; because of this, Arrows may be used for metaprogramming only when the guest language is a superset of the host language. This restriction is also present in multi-level languages which offer unlimited cross-level persistence. <p> This paper introduces generalized arrows and proves that they generalize Arrows in the following sense: every Arrow in a programming language arises from a generalized arrow with that language's term category as its codomain. Generalized arrows impose no containment relationship between the guest language and host language; they facilitate heterogeneous metaprogramming. The category having all generalized arrows as its morphisms and the category having all multi-level languages as its morphisms are isomorphic categories. This is proven formally in Coq, and the proof is offered as justification for the assertion that multi-level languages are generalized arrows. <p> Combined with the existence of a particular kind of retraction in the host language, this proof can be used to define an invertible translation from two-level terms to one-level terms parameterized by a generalized arrow instance. This is ergonomically significant: it lets guest language providers write generalized arrow instances while the users of those guest languages write multi-level terms. This is beneficial because implementing a generalized arrow instance is easier than modifying a compiler, whereas writing two-level terms is easier than manipulating generalized arrow terms.
Purely Functional Structured Programming
Venue: arXiv cs.PL 2011
Year: 2011

The idea of functional programming has played a big role in shaping today's landscape of mainstream programming languages. Another concept that dominates the current programming style is Dijkstra's structured programming. Both concepts have been successfully married, for example in the programming language Scala. This paper proposes how the same can be achieved for structured programming and PURELY functional programming via the notion of LINEAR SCOPE. One advantage of this proposal is that mainstream programmers can reap the benefits of purely functional programming like easily exploitable parallelism while using familiar structured programming syntax and without knowing concepts like monads. A second advantage is that professional purely functional programmers can often avoid hard to read functional code by using structured programming syntax that is often easier to parse mentally.
AntiJam: Efficient Medium Access despite Adaptive and Reactive Jamming
Venue: arXiv cs.DS 2011
Year: 2011

Intentional interference constitutes a major threat for communication networks operating over a shared medium where availability is imperative. Jamming attacks are often simple and cheap to implement. In particular, today's jammers can perform physical carrier sensing in order to disrupt communication more efficiently, specially in a network of simple wireless devices such as sensor nodes, which usually operate over a single frequency (or a limited frequency band) and which cannot benefit from the use of spread spectrum or other more advanced technologies. This article proposes the medium access (MAC) protocol \textsc{AntiJam} that is provably robust against a powerful reactive adversary who can jam a $(1-ε)$-portion of the time steps, where $ε$ is an arbitrary constant. The adversary uses carrier sensing to make informed decisions on when it is most harmful to disrupt communications; moreover, we allow the adversary to be adaptive and to have complete knowledge of the entire protocol history. Our MAC protocol is able to make efficient use of the non-jammed time periods and achieves an asymptotically optimal, $Θ{(1)}$-competitive throughput in this harsh scenario. In addition, \textsc{AntiJam} features a low convergence time and has good fairness properties. Our simulation results validate our theoretical results and also show that our algorithm manages to guarantee constant throughput where the 802.11 MAC protocol basically fails to deliver any packets.
Distributed Source Coding of Correlated Gaussian Sources
Venue: arXiv cs.IT 2011
Year: 2011

We consider the distributed source coding system of $L$ correlated Gaussian sources $Y_i,i=1,2,...,L$ which are noisy observations of correlated Gaussian remote sources $X_k, k=1,2,...,K$. We assume that $Y^{L}={}^{\rm t}(Y_1,Y_2,$ $..., Y_L)$ is an observation of the source vector $X^K={}^{\rm t}(X_1,X_2,..., X_K)$, having the form $Y^L=AX^K+N^L$, where $A$ is a $L\times K$ matrix and $N^L={}^{\rm t}(N_1,N_2,...,N_L)$ is a vector of $L$ independent Gaussian random variables also independent of $X^K$. In this system $L$ correlated Gaussian observations are separately compressed by $L$ encoders and sent to the information processing center. We study the remote source coding problem where the decoder at the center attempts to reconstruct the remote source $X^K$. We consider three distortion criteria based on the covariance matrix of the estimation error on $X^K$. For each of those three criteria we derive explicit inner and outer bounds of the rate distortion region. Next, in the case of $K=L$ and $A=I_L$, we study the multiterminal source coding problem where the decoder wishes to reconstruct the observation $Y^L=X^L+N^L$. To investigate this problem we shall establish a result which provides a strong connection between the remote source coding problem and the multiterminal source coding problem. Using this result, we drive several new partial solutions to the multiterminal source coding problem.
Optimal Base Encodings for Pseudo-Boolean Constraints
Venue: arXiv cs.DM 2011
Year: 2011

This paper formalizes the optimal base problem, presents an algorithm to solve it, and describes its application to the encoding of Pseudo-Boolean constraints to SAT. We demonstrate the impact of integrating our algorithm within the Pseudo-Boolean constraint solver MINISAT+. Experimentation indicates that our algorithm scales to bases involving numbers up to 1,000,000, improving on the restriction in MINISAT+ to prime numbers up to 17. We show that, while for many examples primes up to 17 do suffice, encoding with respect to optimal bases reduces the CNF sizes and improves the subsequent SAT solving time for many examples.