OpenRaiser/Intern-Atlas huggingface dataset:
HordeSat: A Massively Parallel Portfolio SAT Solver
Venue: arXiv cs.LO 2015
Year: 2015

A simple yet successful approach to parallel satisfiability (SAT) solving is to run several different (a portfolio of) SAT solvers on the input problem at the same time until one solver finds a solution. The SAT solvers in the portfolio can be instances of a single solver with different configuration settings. Additionally the solvers can exchange information usually in the form of clauses. In this paper we investigate whether this approach is applicable in the case of massively parallel SAT solving. Our solver is intended to run on clusters with thousands of processors, hence the name HordeSat. HordeSat is a fully distributed portfolio-based SAT solver with a modular design that allows it to use any SAT solver that implements a given interface. HordeSat has a decentralized design and features hierarchical parallelism with interleaved communication and search. We experimentally evaluated it using all the benchmark problems from the application tracks of the 2011 and 2014 International SAT Competitions. The experiments demonstrate that HordeSat is scalable up to hundreds or even thousands of processors achieving significant speedups especially for hard instances.
A Database of $\mathbb{Z}_4$ Codes
Venue: arXiv cs.IT 2015
Year: 2015

There has been much research on codes over $\mathbb{Z}_4$, sometimes called quaternary codes, for over a decade. Yet, no database is available for best known quaternary codes. This work introduces a new database for quaternary codes. It also presents a new search algorithm called genetic code search (GCS), as well as new quaternary codes obtained by existing and new search methods.
Beating the random assignment on constraint satisfaction problems of bounded degree
Venue: arXiv cs.CC 2015
Year: 2015

We show that for any odd $k$ and any instance of the Max-kXOR constraint satisfaction problem, there is an efficient algorithm that finds an assignment satisfying at least a $\frac{1}{2} + Ω(1/\sqrt{D})$ fraction of constraints, where $D$ is a bound on the number of constraints that each variable occurs in. This improves both qualitatively and quantitatively on the recent work of Farhi, Goldstone, and Gutmann (2014), which gave a \emph{quantum} algorithm to find an assignment satisfying a $\frac{1}{2} + Ω(D^{-3/4})$ fraction of the equations. For arbitrary constraint satisfaction problems, we give a similar result for "triangle-free" instances; i.e., an efficient algorithm that finds an assignment satisfying at least a $μ+ Ω(1/\sqrt{D})$ fraction of constraints, where $μ$ is the fraction that would be satisfied by a uniformly random assignment.
Performance Analysis of Ambient RF Energy Harvesting with Repulsive Point Process Modeling
Venue: arXiv cs.NI 2015
Year: 2015

Ambient RF (Radio Frequency) energy harvesting technique has recently been proposed as a potential solution to provide proactive energy replenishment for wireless devices. This paper aims to analyze the performance of a battery-free wireless sensor powered by ambient RF energy harvesting using a stochastic geometry approach. Specifically, we consider the point-to-point uplink transmission of a wireless sensor in a stochastic geometry network, where ambient RF sources, such as mobile transmit devices, access points and base stations, are distributed as a Ginibre alpha-determinantal point process (DPP). The DPP is able to capture repulsion among points, and hence, it is more general than the Poisson point process (PPP). We analyze two common receiver architectures: separated receiver and time-switching architectures. For each architecture, we consider the scenarios with and without co-channel interference for information transmission. We derive the expectation of the RF energy harvesting rate in closed form and also compute its variance. Moreover, we perform a worst-case study which derives the upper bound of both power and transmission outage probabilities. Additionally, we provide guidelines on the setting of optimal time-switching coefficient in the case of the time-switching architecture. Numerical results verify the correctness of the analysis and show various tradeoffs between parameter setting. Lastly, we prove that the sensor is more efficient when the distribution of the ambient sources exhibits stronger repulsion.
The Weakest Failure Detector for Eventual Consistency
Venue: arXiv cs.DC 2015
Year: 2015

In its classical form, a consistent replicated service requires all replicas to witness the same evolution of the service state. Assuming a message-passing environment with a majority of correct processes, the necessary and sufficient information about failures for implementing a general state machine replication scheme ensuring consistency is captured by the Ω failure detector. This paper shows that in such a message-passing environment, Ω is also the weakest failure detector to implement an eventually consistent replicated service, where replicas are expected to agree on the evolution of the service state only after some (a priori unknown) time. In fact, we show that Ω is the weakest to implement eventual consistency in any message-passing environment, i.e., under any assumption on when and where failures might occur. Ensuring (strong) consistency in any environment requires, in addition to Ω, the quorum failure detector Σ. Our paper thus captures, for the first time, an exact computational difference be- tween building a replicated state machine that ensures consistency and one that only ensures eventual consistency.
Content-type coding
Venue: arXiv cs.IT 2015
Year: 2015

This paper is motivated by the observation that, in many cases, we do not need to serve specific messages, but rather, any message within a content-type. Content-type traffic pervades a host of applications today, ranging from search engines and recommender networks to newsfeeds and advertisement networks. The paper asks a novel question: if there are benefits in designing network and channel codes specifically tailored to content-type requests. It provides three examples of content-type formulations to argue that, indeed in some cases we can have significant such benefits.
A Connectivity-Aware Multi-level Finite-Element System for Solving Laplace-Beltrami Equations
Venue: arXiv cs.GR 2015
Year: 2015

Recent work on octree-based finite-element systems has developed a multigrid solver for Poisson equations on meshes. While the idea of defining a regularly indexed function space has been successfully used in a number of applications, it has also been noted that the richness of the function space is limited because the function values can be coupled across locally disconnected regions. In this work, we show how to enrich the function space by introducing functions that resolve the coupling while still preserving the nesting hierarchy that supports multigrid. A spectral analysis reveals the superior quality of the resulting Laplace-Beltrami operator and applications to surface flow demonstrate that our new solver more efficiently converges to the correct solution.
On the Relative Usefulness of Fireballs
Venue: arXiv cs.LO 2015
Year: 2015

In CSL-LICS 2014, Accattoli and Dal Lago showed that there is an implementation of the ordinary (i.e. strong, pure, call-by-name) $λ$-calculus into models like RAM machines which is polynomial in the number of $β$-steps, answering a long-standing question. The key ingredient was the use of a calculus with useful sharing, a new notion whose complexity was shown to be polynomial, but whose implementation was not explored. This paper, meant to be complementary, studies useful sharing in a call-by-value scenario and from a practical point of view. We introduce the Fireball Calculus, a natural extension of call-by-value to open terms for which the problem is as hard as for the ordinary lambda-calculus. We present three results. First, we adapt the solution of Accattoli and Dal Lago, improving the meta-theory of useful sharing. Then, we refine the picture by introducing the GLAMoUr, a simple abstract machine implementing the Fireball Calculus extended with useful sharing. Its key feature is that usefulness of a step is tested---surprisingly---in constant time. Third, we provide a further optimization that leads to an implementation having only a linear overhead with respect to the number of $β$-steps.
Counting Branches in Trees Using Games
Venue: arXiv cs.FL 2015
Year: 2015

We study finite automata running over infinite binary trees. A run of such an automaton is usually said to be accepting if all its branches are accepting. In this article, we relax the notion of accepting run by allowing a certain quantity of rejecting branches. More precisely we study the following criteria for a run to be accepting: - it contains at most finitely (resp countably) many rejecting branches; - it contains infinitely (resp uncountably) many accepting branches; - the set of accepting branches is topologically "big". In all situations we provide a simple acceptance game that later permits to prove that the languages accepted by automata with cardinality constraints are always $ω$-regular. In the case (ii) where one counts accepting branches it leads to new proofs (without appealing to logic) of an old result of Beauquier and Niwinski.
Using Ensemble Models in the Histological Examination of Tissue Abnormalities
Venue: arXiv cs.CV 2015
Year: 2015

Classification models for the automatic detection of abnormalities on histological samples do exists, with an active debate on the cost associated with false negative diagnosis (underdiagnosis) and false positive diagnosis (overdiagnosis). Current models tend to underdiagnose, failing to recognize a potentially fatal disease. The objective of this study is to investigate the possibility of automatically identifying abnormalities in tissue samples through the use of an ensemble model on data generated by histological examination and to minimize the number of false negative cases.
Asymptotically Optimal Planning by Feasible Kinodynamic Planning in State-Cost Space
Venue: arXiv cs.RO 2015
Year: 2015

This paper presents an equivalence between feasible kinodynamic planning and optimal kinodynamic planning, in that any optimal planning problem can be transformed into a series of feasible planning problems in a state-cost space whose solutions approach the optimum. This transformation gives rise to a meta-algorithm that produces an asymptotically optimal planner, given any feasible kinodynamic planner as a subroutine. The meta-algorithm is proven to be asymptotically optimal, and a formula is derived relating expected running time and solution suboptimality. It is directly applicable to a wide range of optimal planning problems because it does not resort to the use of steering functions or numerical boundary-value problem solvers. On a set of benchmark problems, it is demonstrated to perform, using the EST and RRT algorithms as subroutines, at a superior or comparable level to related planners.
OntoSOC: Sociocultural Knowledge Ontology
Venue: arXiv cs.AI 2015
Year: 2015

This paper presents a sociocultural knowledge ontology (OntoSOC) modeling approach. OntoSOC modeling approach is based on Engestrom Human Activity Theory (HAT). That Theory allowed us to identify fundamental concepts and relationships between them. The top-down precess has been used to define differents sub-concepts. The modeled vocabulary permits us to organise data, to facilitate information retrieval by introducing a semantic layer in social web platform architecture, we project to implement. This platform can be considered as a collective memory and Participative and Distributed Information System (PDIS) which will allow Cameroonian communities to share an co-construct knowledge on permanent organized activities.
Margins, Kernels and Non-linear Smoothed Perceptrons
Venue: arXiv cs.LG 2015
Year: 2015

We focus on the problem of finding a non-linear classification function that lies in a Reproducing Kernel Hilbert Space (RKHS) both from the primal point of view (finding a perfect separator when one exists) and the dual point of view (giving a certificate of non-existence), with special focus on generalizations of two classical schemes - the Perceptron (primal) and Von-Neumann (dual) algorithms. We cast our problem as one of maximizing the regularized normalized hard-margin ($ρ$) in an RKHS and %use the Representer Theorem to rephrase it in terms of a Mahalanobis dot-product/semi-norm associated with the kernel's (normalized and signed) Gram matrix. We derive an accelerated smoothed algorithm with a convergence rate of $\tfrac{\sqrt {\log n}}ρ$ given $n$ separable points, which is strikingly similar to the classical kernelized Perceptron algorithm whose rate is $\tfrac1{ρ^2}$. When no such classifier exists, we prove a version of Gordan's separation theorem for RKHSs, and give a reinterpretation of negative margins. This allows us to give guarantees for a primal-dual algorithm that halts in $\min\{\tfrac{\sqrt n}{|ρ|}, \tfrac{\sqrt n}ε\}$ iterations with a perfect separator in the RKHS if the primal is feasible or a dual $ε$-certificate of near-infeasibility.
Consistent Algorithms for Multiclass Classification with a Reject Option
Venue: arXiv cs.LG 2015
Year: 2015

We consider the problem of $n$-class classification ($n\geq 2$), where the classifier can choose to abstain from making predictions at a given cost, say, a factor $α$ of the cost of misclassification. Designing consistent algorithms for such $n$-class classification problems with a `reject option' is the main goal of this paper, thereby extending and generalizing previously known results for $n=2$. We show that the Crammer-Singer surrogate and the one vs all hinge loss, albeit with a different predictor than the standard argmax, yield consistent algorithms for this problem when $α=\frac{1}{2}$. More interestingly, we design a new convex surrogate that is also consistent for this problem when $α=\frac{1}{2}$ and operates on a much lower dimensional space ($\log(n)$ as opposed to $n$). We also generalize all three surrogates to be consistent for any $α\in[0, \frac{1}{2}]$.
WhittleSearch: Interactive Image Search with Relative Attribute Feedback
Venue: arXiv cs.CV 2015
Year: 2015

We propose a novel mode of feedback for image search, where a user describes which properties of exemplar images should be adjusted in order to more closely match his/her mental model of the image sought. For example, perusing image results for a query "black shoes", the user might state, "Show me shoe images like these, but sportier." Offline, our approach first learns a set of ranking functions, each of which predicts the relative strength of a nameable attribute in an image (e.g., sportiness). At query time, the system presents the user with a set of exemplar images, and the user relates them to his/her target image with comparative statements. Using a series of such constraints in the multi-dimensional attribute space, our method iteratively updates its relevance function and re-ranks the database of images. To determine which exemplar images receive feedback from the user, we present two variants of the approach: one where the feedback is user-initiated and another where the feedback is actively system-initiated. In either case, our approach allows a user to efficiently "whittle away" irrelevant portions of the visual feature space, using semantic language to precisely communicate her preferences to the system. We demonstrate our technique for refining image search for people, products, and scenes, and we show that it outperforms traditional binary relevance feedback in terms of search speed and accuracy. In addition, the ordinal nature of relative attributes helps make our active approach efficient -- both computationally for the machine when selecting the reference images, and for the user by requiring less user interaction than conventional passive and active methods.
Greedy Matching: Guarantees and Limitations
Venue: arXiv cs.DS 2015
Year: 2015

Since Tinhofer proposed the MinGreedy algorithm for maximum cardinality matching in 1984, several experimental studies found the randomized algorithm to perform excellently for various classes of random graphs and benchmark instances. In contrast, only few analytical results are known. We show that MinGreedy cannot improve on the trivial approximation ratio 1/2 whp., even for bipartite graphs. Our hard inputs seem to require a small number of high-degree nodes. This motivates an investigation of greedy algorithms on graphs with maximum degree D: We show that MinGreedy achieves a (D-1)/(2D-3)-approximation for graphs with D=3 and for D-regular graphs, and a guarantee of (D-1/2)/(2D-2) for graphs with maximum degree D. Interestingly, our bounds even hold for the deterministic MinGreedy that breaks all ties arbitrarily. Moreover, we investigate the limitations of the greedy paradigm, using the model of priority algorithms introduced by Borodin, Nielsen, and Rackoff. We study deterministic priority algorithms and prove a (D-1)/(2D-3)-inapproximability result for graphs with maximum degree D; thus, these greedy algorithms do not achieve a 1/2+eps-approximation and in particular the 2/3-approximation obtained by the deterministic MinGreedy for D=3 is optimal in this class. For k-uniform hypergraphs we show a tight 1/k-inapproximability bound. We also study fully randomized priority algorithms and give a 5/6-inapproximability bound. Thus, they cannot compete with matching algorithms of other paradigms.
Container Relocation Problem: Approximation, Asymptotic, and Incomplete Information
Venue: arXiv cs.DS 2015
Year: 2015

The Container Relocation Problem (CRP) is concerned with finding a sequence of moves of containers that minimizes the number of relocations needed to retrieve all containers respecting a given order of retrieval. While the problem is known to be NP-hard, certain algorithms such as the A* search and heuristics perform reasonably well on many instances of the problem. In this paper, we first focus on the A* search algorithm, and analyze lower and upper bounds that are easy to compute and can be used to prune nodes. Our analysis sheds light on which bounds result in fast computation within a given approximation gap. We present extensive simulation results that improve upon our theoretical analysis, and further show that our method finds the optimum solution on most instances of medium-size bays. On "hard" instances, our method finds an approximate solution with a small gap and within a time frame that is fast for practical applications. We also study the average-case asymptotic behavior of the CRP where the number of columns grows. We calculate the expected number of relocations in the limit, and show that the optimum number of relocations converges to a simple and intuitive lower-bound. We further study the CRP with incomplete information by relaxing the assumption that the order of retrieval of all containers are initially known. This assumption is particularly unrealistic in ports without an appointment system. We assume that the retrieval order of a subset of containers is known initially and the retrieval order of the remaining containers is observed later at a given specific time. Before this time, we assume a probabilistic distribution on the retrieval order of unknown containers. We combine the A* algorithm with sampling technique to solve this two-stage stochastic optimization problem. We show that our algorithm is fast and the error due to sampling and pruning is reasonably small.
Robust Real-time Extraction of Fiducial Facial Feature Points using Haar-like Features
Venue: arXiv cs.CV 2015
Year: 2015

In this paper, we explore methods of robustly extracting fiducial facial feature points - an important process for numerous facial image processing tasks. We consider various methods to first detect face, then facial features and finally salient facial feature points. Colour-based models are analysed and their overall unsuitability for this task is summarised. The bulk of the report is then dedicated to proposing a learning-based method centred on the Viola-Jones algorithm. The specific difficulties and considerations relating to feature point detection are laid out in this context and a novel approach is established to address these issues. On a sequence of clear and unobstructed face images, our proposed system achieves average detection rates of over 90%. Then, using a more varied sample dataset, we identify some possible areas for future development of our system.
Elaboration in Dependent Type Theory
Venue: arXiv cs.LO 2015
Year: 2015

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean's elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved.
Low-rank correction methods for algebraic domain decomposition preconditioners
Venue: arXiv cs.NA 2015
Year: 2015

This paper presents a parallel preconditioning method for distributed sparse linear systems, based on an approximate inverse of the original matrix, that adopts a general framework of distributed sparse matrices and exploits the domain decomposition method and low-rank corrections. The domain decomposition approach decouples the matrix and once inverted, a low-rank approximation is applied by exploiting the Sherman-Morrison-Woodbury formula, which yields two variants of the preconditioning methods. The low-rank expansion is computed by the Lanczos procedure with reorthogonalizations. Numerical experiments indicate that, when combined with Krylov subspace accelerators, this preconditioner can be efficient and robust for solving symmetric sparse linear systems. Comparisons with other distributed-memory preconditioning methods are presented.
Simultaneous Visibility Representations of Plane st-graphs Using L-shapes
Venue: arXiv cs.CG 2015
Year: 2015

Let $\langle G_r,G_b \rangle$ be a pair of plane $st$-graphs with the same vertex set $V$. A simultaneous visibility representation with L-shapes of $\langle G_r,G_b \rangle$ is a pair of bar visibility representations $\langleΓ_r,Γ_b\rangle$ such that, for every vertex $v \in V$, $Γ_r(v)$ and $Γ_b(v)$ are a horizontal and a vertical segment, which share an end-point. In other words, every vertex is drawn as an $L$-shape, every edge of $G_r$ is a vertical visibility segment, and every edge of $G_b$ is a horizontal visibility segment. Also, no two L-shapes intersect each other. An L-shape has four possible rotations, and we assume that each vertex is given a rotation for its L-shape as part of the input. Our main results are: (i) a characterization of those pairs of plane $st$-graphs admitting such a representation, (ii) a cubic time algorithm to recognize them, and (iii) a linear time drawing algorithm if the test is positive.