OpenRaiser/Intern-Atlas huggingface dataset:
Proof Complexity and the Kneser-Lovász Theorem
Venue: arXiv cs.CC 2018
Year: 2018

We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovász Theorem. This is a family of propositional tautologies, indexed by an nonnegative integer parameter $k$ that generalizes the Pigeonhole Principle (obtained for $k=1$). We show, for all fixed $k$, $2^{Ω(n)}$ lower bounds on resolution complexity and exponential lower bounds for bounded depth Frege proofs. These results hold even for the more restricted class of formulas encoding Schrijver's strenghtening of the Kneser-Lovász Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the Kneser-Lovász Theorem are known) we give polynomial size Frege ($k=2$), respectively extended Frege ($k=3$) proofs. The paper concludes with a brief announcement of the results (presented in subsequent work) on the proof complexity of the general case of the Kneser-Lovász theorem.
The Anatomy of a Modular System for Media Content Analysis
Venue: arXiv cs.MA 2018
Year: 2018

Intelligent systems for the annotation of media content are increasingly being used for the automation of parts of social science research. In this domain the problem of integrating various Artificial Intelligence (AI) algorithms into a single intelligent system arises spontaneously. As part of our ongoing effort in automating media content analysis for the social sciences, we have built a modular system by combining multiple AI modules into a flexible framework in which they can cooperate in complex tasks. Our system combines data gathering, machine translation, topic classification, extraction and annotation of entities and social networks, as well as many other tasks that have been perfected over the past years of AI research. Over the last few years, it has allowed us to realise a series of scientific studies over a vast range of applications including comparative studies between news outlets and media content in different countries, modelling of user preferences, and monitoring public mood. The framework is flexible and allows the design and implementation of modular agents, where simple modules cooperate in the annotation of a large dataset without central coordination.
Spectral concentration and greedy k-clustering
Venue: arXiv cs.DS 2018
Year: 2018

A popular graph clustering method is to consider the embedding of an input graph into R^k induced by the first k eigenvectors of its Laplacian, and to partition the graph via geometric manipulations on the resulting metric space. Despite the practical success of this methodology, there is limited understanding of several heuristics that follow this framework. We provide theoretical justification for one such natural and computationally efficient variant. Our result can be summarized as follows. A partition of a graph is called strong if each cluster has small external conductance, and large internal conductance. We present a simple greedy spectral clustering algorithm which returns a partition that is provably close to a suitably strong partition, provided that such a partition exists. A recent result shows that strong partitions exist for graphs with a sufficiently large spectral gap between the k-th and (k+1)-st eigenvalues. Taking this together with our main theorem gives a spectral algorithm which finds a partition close to a strong one for graphs with large enough spectral gap. We also show how this simple greedy algorithm can be implemented in near-linear time for any fixed k and error guarantee. Finally, we evaluate our algorithm on some real-world and synthetic inputs.
A Bayes consistent 1-NN classifier
Venue: arXiv cs.LG 2018
Year: 2018

We show that a simple modification of the 1-nearest neighbor classifier yields a strongly Bayes consistent learner. Prior to this work, the only strongly Bayes consistent proximity-based method was the k-nearest neighbor classifier, for k growing appropriately with sample size. We will argue that a margin-regularized 1-NN enjoys considerable statistical and algorithmic advantages over the k-NN classifier. These include user-friendly finite-sample error bounds, as well as time- and memory-efficient learning and test-point evaluation algorithms with a principled speed-accuracy tradeoff. Encouraging empirical results are reported.
Stable Throughput Region of Cognitive-Relay Networks with Imperfect Sensing and Finite Relaying Buffer
Venue: arXiv cs.NI 2018
Year: 2018

In this letter, we obtain the stable throughput region for a cognitive relaying scheme with a finite relaying buffer and imperfect sensing. The analysis investigates the effect of the secondary user's finite relaying capabilities under different scenarios of primary, secondary and relaying links outages. Furthermore, we demonstrate the effect of miss detection and false alarm probabilities on the achievable throughput for the primary and secondary users.
On the neighbour sum distinguishing index of planar graphs
Venue: arXiv cs.DM 2018
Year: 2018

Let $c$ be a proper edge colouring of a graph $G=(V,E)$ with integers $1,2,\ldots,k$. Then $k\geq Δ(G)$, while by Vizing's theorem, no more than $k=Δ(G)+1$ is necessary for constructing such $c$. On the course of investigating irregularities in graphs, it has been moreover conjectured that only slightly larger $k$, i.e., $k=Δ(G)+2$ enables enforcing additional strong feature of $c$, namely that it attributes distinct sums of incident colours to adjacent vertices in $G$ if only this graph has no isolated edges and is not isomorphic to $C_5$. We prove the conjecture is valid for planar graphs of sufficiently large maximum degree. In fact even stronger statement holds, as the necessary number of colours stemming from the result of Vizing is proved to be sufficient for this family of graphs. Specifically, our main result states that every planar graph $G$ of maximum degree at least $28$ which contains no isolated edges admits a proper edge colouring $c:E\to\{1,2,\ldots,Δ(G)+1\}$ such that $\sum_{e\ni u}c(e)\neq \sum_{e\ni v}c(e)$ for every edge $uv$ of $G$.
A Game Theoretic Model for the Formation of Navigable Small-World Networks --- the Tradeoff between Distance and Reciprocity
Venue: arXiv cs.SI 2018
Year: 2018

Kleinberg proposed a family of small-world networks to explain the navigability of large-scale real-world social networks. However, the underlying mechanism that drives real networks to be navigable is not yet well understood. In this paper, we present a game theoretic model for the formation of navigable small world networks. We model the network formation as a Distance-Reciprocity Balanced (DRB) game in which people seek for both high reciprocity and long-distance relationships. We show that the game has only two Nash equilibria: One is the navigable small-world network, and the other is the random network in which each node connects with each other node with equal probability. We further show that the navigable small world is very stable --- (a) no collusion of any size would benefit from deviating from it; and (b) after an arbitrary deviations of a large random set of nodes, the network would return to the navigable small world as soon as every node takes one best-response step. In contrast, for the random network, a small group collusion or random perturbations is guaranteed to move the network to the navigable network as soon as every node takes one best-response step. Moreover, we show that navigable small world has much better social welfare than the random network, and provide the price-of-anarchy and price-of-stability results of the game. Our empirical evaluation demonstrates that the system always converges to the navigable network even when limited or no information about other players' strategies is available, and the DRB game simulated on the real-world network leads to navigability characteristic that is very close to that of the real network. Our theoretical and empirical analyses provide important new insight on the connection between distance, reciprocity and navigability in social networks.
Approximate MAP Estimation for Pairwise Potentials via Baker's Technique
Venue: arXiv cs.DS 2018
Year: 2018

The theoretical models providing mathematical abstractions for several significant optimization problems in machine learning, combinatorial optimization, computer vision and statistical physics have intrinsic similarities. We propose a unified framework to model these computation tasks where the structures of these optimization problems are encoded by functions attached on the vertices and edges of a graph. We show that computing MAX 2-CSP admits polynomial-time approximation scheme (PTAS) on planar graphs, graphs with bounded local treewidth, $H$-minor-free graphs, geometric graphs with bounded density and graphs embeddable with bounded number of crossings per edge. This implies computing MAX-CUT, MAX-DICUT and MAX $k$-CUT admits PTASs on all these classes of graphs. Our method also gives the first PTAS for computing the ground state of ferromagnetic Edwards-Anderson model without external magnetic field on $d$-dimensional lattice graphs. These results are widely applicable in vision, graphics and machine learning.
Enumerative Coding for Line Polar Grassmannians with applications to codes
Venue: arXiv cs.IT 2018
Year: 2018

A $k$-polar Grassmannian is the geometry having as pointset the set of all $k$-dimensional subspaces of a vector space $V$ which are totally isotropic for a given non-degenerate bilinear form $μ$ defined on $V.$ Hence it can be regarded as a subgeometry of the ordinary $k$-Grassmannian. In this paper we deal with orthogonal line Grassmannians and with symplectic line Grassmannians, i.e. we assume $k=2$ and $μ$ a non-degenerate symmetric or alternating form. We will provide a method to efficiently enumerate the pointsets of both orthogonal and symplectic line Grassmannians. This has several nice applications; among them, we shall discuss an efficient encoding/decoding/error correction strategy for line polar Grassmann codes of both types.
Varieties
Venue: arXiv cs.FL 2018
Year: 2018

This text is devoted to the theory of varieties, which provides an important tool, based in universal algebra, for the classification of regular languages. In the introductory section, we present a number of examples that illustrate and motivate the fundamental concepts. We do this for the most part without proofs, and often without precise definitions, leaving these to the formal development of the theory that begins in Section 2. Our presentation of the theory draws heavily on the work of Gehrke, Grigorieff and Pin (2008) on the equational theory of lattices of regular languages. In the subsequent sections we consider in more detail aspects of varieties that were only briefly evoked in the introduction: Decidability, operations on languages, and characterizations in formal logic.
SybilFrame: A Defense-in-Depth Framework for Structure-Based Sybil Detection
Venue: arXiv cs.SI 2018
Year: 2018

Sybil attacks are becoming increasingly widespread, and pose a significant threat to online social systems; a single adversary can inject multiple colluding identities in the system to compromise security and privacy. Recent works have leveraged the use of social network-based trust relationships to defend against Sybil attacks. However, existing defenses are based on oversimplified assumptions, which do not hold in real world social graphs. In this work, we propose SybilFrame, a defense-in-depth framework for mitigating the problem of Sybil attacks when the oversimplified assumptions are relaxed. Our framework is able to incorporate prior information about users and edges in the social graph. We validate our framework on synthetic and real world network topologies, including a large-scale Twitter dataset with 20M nodes and 265M edges, and demonstrate that our scheme performs an order of magnitude better than previous structure-based approaches.
IMP with exceptions over decorated logic
Venue: arXiv cs.LO 2018
Year: 2018

In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with `decorations' that describe what computational (side) effect evaluation of a term may involve. In a point-free categorical language,called the `decorated logic', we formalize the mutable state and the exception effects first separately, exploiting anice duality between them, and then combined. The combined decorated logic is used as the target language forthe denotational semantics of the IMP+Exc imperative programming language, and allows us to prove equivalencesbetween programs written in IMP+Exc. The combined logic is encoded in Coq, and this encoding is used to certifysome program equivalence proofs.
Geometry of Interaction for MALL via Hughes-vanGlabbeek Proof-Nets
Venue: arXiv cs.LO 2018
Year: 2018

This paper presents, for the first time, a Geometry of Interaction (GoI) interpretation inspired from Hughes-vanGlabbeek (HvG) proof-nets for multiplicative additive linear logic (MALL). Our GoI dynamically captures HvG's geometric correctness criterion-the toggling cycle condition-in terms of algebraic operators. Our new ingredient is a scalar extension of the *-algebra in Girard's *-ring of partial isometries over a boolean polynomial ring with literals of eigenweights as indeterminates. In order to capture feedback arising from cuts, we construct a finer grained execution formula. The expansion of this execution formula is longer than that for collections of slices for multiplicative GoI, hence it is harder to prove termination. Our GoI gives a dynamical, semantical account of boolean valuations (in particular, pruning sub-proofs), conversion of weights (in particular, alpha-conversion), and additive (co)contraction, peculiar to additive proof-theory. Termination of our execution formula is shown to correspond to HvG's toggling criterion. The slice-wise restriction of our execution formula (by collapsing the boolean structure) yields the well known correspondence, explicit or implicit in previous works on multiplicative GoI, between the convergence of execution formulas and acyclicity of proof-nets. Feedback arising from the execution formula by restricting to the boolean polynomial structure yields autonomous definability of eigenweights among cuts from the rest of the eigenweights.
Complete Simulation of Automata Networks
Venue: arXiv cs.FL 2018
Year: 2018

Consider a finite set $A$ and an integer $n \geq 1$. This paper studies the concept of complete simulation in the context of semigroups of transformations of $A^n$, also known as finite state-homogeneous automata networks. For $m \geq n$, a transformation of $A^m$ is \emph{$n$-complete of size $m$} if it may simulate every transformation of $A^n$ by updating one coordinate (or register) at a time. Using tools from memoryless computation, it is established that there is no $n$-complete transformation of size $n$, but there is such a transformation of size $n+1$. By studying the the time of simulation of various $n$-complete transformations, it is conjectured that the maximal time of simulation of any $n$-complete transformation is at least $2n$. A transformation of $A^m$ is \emph{sequentially $n$-complete of size $m$} if it may sequentially simulate every finite sequence of transformations of $A^n$; in this case, minimal examples and bounds for the size and time of simulation are determined. It is also shown that there is no $n$-complete transformation that updates all the registers in parallel, but that there exists a sequentally $n$-complete transformation that updates all but one register in parallel. This illustrates the strengths and weaknesses of parallel models of computation, such as cellular automata.
Anxiety, Alcohol, and Academics: A Textual Analysis of Student Facebook Confessions Pages
Venue: arXiv cs.SI 2018
Year: 2018

What do college students reveal to their peers on social media under complete anonymity? Do their campus environments relate to the topics of their disclosure? To answer these questions, I analyze Facebook confessions pages. Popular on hundreds of college campuses, these pages allow students to anonymously post personal confessions on a public community forum. In this preliminary research note, I analyze several explanatory factors of online student confessional behavior. Aggregating nearly 200,000 confessions posts spanning a period of 3 years, I combine Latent Dirichlet Allocation (LDA) with human verification through Mechanical Turk to scalably identify topics in these online confessions. Where possible, I also link posts to real-world news events parsed from Twitter. I find that confessions mentioning socioeconomics as well as mental and physical health occur more often at top-ranking, expensive private colleges. While event-related confessions most often mention timely school-related events, many mention global and domestic events outside of the local campus sphere. Results suggest that undergraduates from different campuses disclose about topics such as race, socioeonomics, and politics differently, but in aggregate, post in similar patterns over time. Additionally, results confirm that anonymous Facebook confessors receive support for confessions on important, but taboo topics such as health and socioeconomic status.
Automata and Quantum Computing
Venue: arXiv cs.FL 2018
Year: 2018

Quantum computing is a new model of computation, based on quantum physics. Quantum computers can be exponentially faster than conventional computers for problems such as factoring. Besides full-scale quantum computers, more restricted models such as quantum versions of finite automata have been studied. In this paper, we survey various models of quantum finite automata and their properties. We also provide some open questions and new directions for researchers. Keywords: quantum finite automata, probabilistic finite automata, nondeterminism, bounded error, unbounded error, state complexity, decidability and undecidability, computational complexity
The Complexity of All-switches Strategy Improvement
Venue: arXiv cs.DS 2018
Year: 2018

Strategy improvement is a widely-used and well-studied class of algorithms for solving graph-based infinite games. These algorithms are parameterized by a switching rule, and one of the most natural rules is "all switches" which switches as many edges as possible in each iteration. Continuing a recent line of work, we study all-switches strategy improvement from the perspective of computational complexity. We consider two natural decision problems, both of which have as input a game $G$, a starting strategy $s$, and an edge $e$. The problems are: 1.) The edge switch problem, namely, is the edge $e$ ever switched by all-switches strategy improvement when it is started from $s$ on game $G$? 2.) The optimal strategy problem, namely, is the edge $e$ used in the final strategy that is found by strategy improvement when it is started from $s$ on game $G$? We show $\mathtt{PSPACE}$-completeness of the edge switch problem and optimal strategy problem for the following settings: Parity games with the discrete strategy improvement algorithm of Vöge and Jurdziński; mean-payoff games with the gain-bias algorithm [14,37]; and discounted-payoff games and simple stochastic games with their standard strategy improvement algorithms. We also show $\mathtt{PSPACE}$-completeness of an analogous problem to edge switch for the bottom-antipodal algorithm for finding the sink of an Acyclic Unique Sink Orientation on a cube.
Topology Control of wireless sensor network using Quantum Inspired Genetic algorithm
Venue: arXiv cs.NE 2018
Year: 2018

In this work, an evolving Linked Quantum register has been introduced, which are group vector of binary pair of genes, which in its local proximity represent those nodes that will have high connectivity and keep the energy consumption at low, and which are taken into account for topology control. The register works in higher dimension. Here order-2 Quantum inspired genetic algorithm has been used and also higher order can be used to achieve greater versatility in topology control of nodes. Numerical result has been obtained, analysis is done as how the result has previously been obtained with Quantum genetic algorithm and results are compared too. For future work, factor is hinted which would exploit the algorithm to work in more computational intensive problem.
Optimized Projections for Compressed Sensing via Direct Mutual Coherence Minimization
Venue: arXiv cs.IT 2018
Year: 2018

Compressed Sensing (CS) is a novel technique for simultaneous signal sampling and compression based on the existence of a sparse representation of signal and a projected dictionary $PD$, where $P\in\mathbb{R}^{m\times d}$ is the projection matrix and $D\in\mathbb{R}^{d\times n}$ is the dictionary. To exactly recover the signal with a small number of measurements $m$, the projected dictionary $PD$ is expected to be of low mutual coherence. Several previous methods attempt to find the projection $P$ such that the mutual coherence of $PD$ can be as low as possible. However, they do not minimize the mutual coherence directly and thus their methods are far from optimal. Also the solvers they used lack of the convergence guarantee and thus there has no guarantee on the quality of their obtained solutions. This work aims to address these issues. We propose to find an optimal projection by minimizing the mutual coherence of $PD$ directly. This leads to a nonconvex nonsmooth minimization problem. We then approximate it by smoothing and solve it by alternate minimization. We further prove the convergence of our algorithm. To the best of our knowledge, this is the first work which directly minimizes the mutual coherence of the projected dictionary with a convergence guarantee. Numerical experiments demonstrate that the proposed method can recover sparse signals better than existing methods.
Logic Programming with Macro Connectives
Venue: arXiv cs.PL 2018
Year: 2018

Logic programming such as Prolog is often sequential and slow because each execution step processes only a single, $micro$ connective. To fix this problem, we propose to use $macro$ connectives as the means of improving both readability and performance.
Incorporating User Interaction into Imperative Languages
Venue: arXiv cs.PL 2018
Year: 2018

In this paper, we present two new forms of the $write$ statement: one of the form $write(x);G$ where $G$ is a statement and the other of the form $write(x);D$ where $D$ is a module. The former is a generalization of traditional $write$ statement and is quite useful. The latter is useful for implementing interactive modules.
Distributed Event-Triggered Control for Asymptotic Synchronization of Dynamical Networks
Venue: arXiv cs.SY 2018
Year: 2018

This paper studies synchronization of dynamical networks with event-based communication. Firstly, two estimators are introduced into each node, one to estimate its own state, and the other to estimate the average state of its neighbours. Then, with these two estimators, a distributed event-triggering rule (ETR) with a dwell time is designed such that the network achieves synchronization asymptotically with no Zeno behaviours. The designed ETR only depends on the information that each node can obtain, and thus can be implemented in a decentralized way.