OpenRaiser/Intern-Atlas huggingface dataset:
Manipulation and gender neutrality in stable marriage procedures
Venue: arXiv cs.AI 2009
Year: 2009

The stable marriage problem is a well-known problem of matching men to women so that no man and woman who are not married to each other both prefer each other. Such a problem has a wide variety of practical applications ranging from matching resident doctors to hospitals to matching students to schools. A well-known algorithm to solve this problem is the Gale-Shapley algorithm, which runs in polynomial time. It has been proven that stable marriage procedures can always be manipulated. Whilst the Gale-Shapley algorithm is computationally easy to manipulate, we prove that there exist stable marriage procedures which are NP-hard to manipulate. We also consider the relationship between voting theory and stable marriage procedures, showing that voting rules which are NP-hard to manipulate can be used to define stable marriage procedures which are themselves NP-hard to manipulate. Finally, we consider the issue that stable marriage procedures like Gale-Shapley favour one gender over the other, and we show how to use voting rules to make any stable marriage procedure gender neutral.
Scalable Inference for Latent Dirichlet Allocation
Venue: arXiv cs.LG 2009
Year: 2009

We investigate the problem of learning a topic model - the well-known Latent Dirichlet Allocation - in a distributed manner, using a cluster of C processors and dividing the corpus to be learned equally among them. We propose a simple approximated method that can be tuned, trading speed for accuracy according to the task at hand. Our approach is asynchronous, and therefore suitable for clusters of heterogenous machines.
A Better Reduction Theorem for Store Buffers
Venue: arXiv cs.LO 2009
Year: 2009

When verifying a concurrent program, it is usual to assume that memory is sequentially consistent. However, most modern multiprocessors depend on store buffering for efficiency, and provide native sequential consistency only at a substantial performance penalty. To regain sequential consistency, a programmer has to follow an appropriate programming discipline. However, naïve disciplines, such as protecting all shared accesses with locks, are not flexible enough for building high-performance multiprocessor software. We present a new discipline for concurrent programming under TSO (total store order, with store buffer forwarding). It does not depend on concurrency primitives, such as locks. Instead, threads use ghost operations to acquire and release ownership of memory addresses. A thread can write to an address only if no other thread owns it, and can read from an address only if it owns it or it is shared and the thread has flushed its store buffer since it last wrote to an address it did not own. This discipline covers both coarse-grained concurrency (where data is protected by locks) as well as fine-grained concurrency (where atomic operations race to memory). We formalize this discipline in Isabelle/HOL, and prove that if every execution of a program in a system without store buffers follows the discipline, then every execution of the program with store buffers is sequentially consistent. Thus, we can show sequential consistency under TSO by ordinary assertional reasoning about the program, without having to consider store buffers at all.
On the Different Shapes Arising in a Family of Rational Curves Depending on a Parameter
Venue: arXiv cs.SC 2009
Year: 2009

Given a family of rational curves depending on a real parameter, defined by its parametric equations, we provide an algorithm to compute a finite partition of the parameter space (${\Bbb R}$, in general) so that the shape of the family stays invariant along each element of the partition. So, from this partition the topology types in the family can be determined. The algorithm is based on a geometric interpretation of previous work (\cite{JGRS}) for the implicit case. However, in our case the algorithm works directly with the parametrization of the family, and the implicit equation does not need to be computed. Timings comparing the algorithm in the implicit and the parametric cases are given; these timings show that the parametric algorithm developed here provides in general better results than the known algorithm for the implicit case.
Event-Driven Optimal Feedback Control for Multi-Antenna Beamforming
Venue: arXiv cs.IT 2009
Year: 2009

Transmit beamforming is a simple multi-antenna technique for increasing throughput and the transmission range of a wireless communication system. The required feedback of channel state information (CSI) can potentially result in excessive overhead especially for high mobility or many antennas. This work concerns efficient feedback for transmit beamforming and establishes a new approach of controlling feedback for maximizing net throughput, defined as throughput minus average feedback cost. The feedback controller using a stationary policy turns CSI feedback on/off according to the system state that comprises the channel state and transmit beamformer. Assuming channel isotropy and Markovity, the controller's state reduces to two scalars. This allows the optimal control policy to be efficiently computed using dynamic programming. Consider the perfect feedback channel free of error, where each feedback instant pays a fixed price. The corresponding optimal feedback control policy is proved to be of the threshold type. This result holds regardless of whether the controller's state space is discretized or continuous. Under the threshold-type policy, feedback is performed whenever a state variable indicating the accuracy of transmit CSI is below a threshold, which varies with channel power. The practical finite-rate feedback channel is also considered. The optimal policy for quantized feedback is proved to be also of the threshold type. The effect of CSI quantization is shown to be equivalent to an increment on the feedback price. Moreover, the increment is upper bounded by the expected logarithm of one minus the quantization error. Finally, simulation shows that feedback control increases net throughput of the conventional periodic feedback by up to 0.5 bit/s/Hz without requiring additional bandwidth or antennas.
Complexity of Strong Implementability
Venue: arXiv cs.CC 2009
Year: 2009

We consider the question of implementability of a social choice function in a classical setting where the preferences of finitely many selfish individuals with private information have to be aggregated towards a social choice. This is one of the central questions in mechanism design. If the concept of weak implementation is considered, the Revelation Principle states that one can restrict attention to truthful implementations and direct revelation mechanisms, which implies that implementability of a social choice function is easy to check. For the concept of strong implementation, however, the Revelation Principle becomes invalid, and the complexity of deciding whether a given social choice function is strongly implementable has been open so far. In this paper, we show by using methods from polyhedral theory that strong implementability of a social choice function can be decided in polynomial space and that each of the payments needed for strong implementation can always be chosen to be of polynomial encoding length. Moreover, we show that strong implementability of a social choice function involving only a single selfish individual can be decided in polynomial time via linear programming.
Deriving SN from PSN: a general proof technique
Venue: arXiv cs.LO 2009
Year: 2009

In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easily proved, only one of them is usually established (and sometimes none). We propose here a connection between them which helps to get SN when one already has PSN. For this purpose, we formalize a general proof technique of SN which consists in expanding substitutions into "pure" lambda-terms and to inherit SN of the whole calculus by SN of the "pure" calculus and by PSN. We apply it successfully to a large set of calculi with explicit substitutions, allowing us to establish SN, or, at least, to trace back the failure of SN to that of PSN.
Random Access Transport Capacity
Venue: arXiv cs.IT 2009
Year: 2009

We develop a new metric for quantifying end-to-end throughput in multihop wireless networks, which we term random access transport capacity, since the interference model presumes uncoordinated transmissions. The metric quantifies the average maximum rate of successful end-to-end transmissions, multiplied by the communication distance, and normalized by the network area. We show that a simple upper bound on this quantity is computable in closed-form in terms of key network parameters when the number of retransmissions is not restricted and the hops are assumed to be equally spaced on a line between the source and destination. We also derive the optimum number of hops and optimal per hop success probability and show that our result follows the well-known square root scaling law while providing exact expressions for the preconstants as well. Numerical results demonstrate that the upper bound is accurate for the purpose of determining the optimal hop count and success (or outage) probability.
Bounding the Sensitivity of Polynomial Threshold Functions
Venue: arXiv cs.CC 2009
Year: 2009

We give the first non-trivial upper bounds on the average sensitivity and noise sensitivity of polynomial threshold functions. More specifically, for a Boolean function f on n variables equal to the sign of a real, multivariate polynomial of total degree d we prove 1) The average sensitivity of f is at most O(n^{1-1/(4d+6)}) (we also give a combinatorial proof of the bound O(n^{1-1/2^d}). 2) The noise sensitivity of f with noise rate δis at most O(δ^{1/(4d+6)}). Previously, only bounds for the linear case were known. Along the way we show new structural theorems about random restrictions of polynomial threshold functions obtained via hypercontractivity. These structural results may be of independent interest as they provide a generic template for transforming problems related to polynomial threshold functions defined on the Boolean hypercube to polynomial threshold functions defined in Gaussian space.
GPU sample sort
Venue: arXiv cs.DS 2009
Year: 2009

In this paper, we present the design of a sample sort algorithm for manycore GPUs. Despite being one of the most efficient comparison-based sorting algorithms for distributed memory architectures its performance on GPUs was previously unknown. For uniformly distributed keys our sample sort is at least 25% and on average 68% faster than the best comparison-based sorting algorithm, GPU Thrust merge sort, and on average more than 2 times faster than GPU quicksort. Moreover, for 64-bit integer keys it is at least 63% and on average 2 times faster than the highly optimized GPU Thrust radix sort that directly manipulates the binary representation of keys. Our implementation is robust to different distributions and entropy levels of keys and scales almost linearly with the input size. These results indicate that multi-way techniques in general and sample sort in particular achieve substantially better performance than two-way merge sort and quicksort.
Supporting Lock-Free Composition of Concurrent Data Objects
Venue: arXiv cs.DC 2009
Year: 2009

Lock-free data objects offer several advantages over their blocking counterparts, such as being immune to deadlocks and convoying and, more importantly, being highly concurrent. But they share a common disadvantage in that the operations they provide are difficult to compose into larger atomic operations while still guaranteeing lock-freedom. We present a lock-free methodology for composing highly concurrent linearizable objects together by unifying their linearization points. This makes it possible to relatively easily introduce atomic lock-free move operations to a wide range of concurrent objects. Experimental evaluation has shown that the operations originally supported by the data objects keep their performance behavior under our methodology.
Accurate low-rank matrix recovery from a small number of linear measurements
Venue: arXiv cs.IT 2009
Year: 2009

We consider the problem of recovering a lowrank matrix M from a small number of random linear measurements. A popular and useful example of this problem is matrix completion, in which the measurements reveal the values of a subset of the entries, and we wish to fill in the missing entries (this is the famous Netflix problem). When M is believed to have low rank, one would ideally try to recover M by finding the minimum-rank matrix that is consistent with the data; this is, however, problematic since this is a nonconvex problem that is, generally, intractable. Nuclear-norm minimization has been proposed as a tractable approach, and past papers have delved into the theoretical properties of nuclear-norm minimization algorithms, establishing conditions under which minimizing the nuclear norm yields the minimum rank solution. We review this spring of emerging literature and extend and refine previous theoretical results. Our focus is on providing error bounds when M is well approximated by a low-rank matrix, and when the measurements are corrupted with noise. We show that for a certain class of random linear measurements, nuclear-norm minimization provides stable recovery from a number of samples nearly at the theoretical lower limit, and enjoys order-optimal error bounds (with high probability).
Combining Approximation Algorithms for the Prize-Collecting TSP
Venue: arXiv cs.DS 2009
Year: 2009

We present a 1.91457-approximation algorithm for the prize-collecting travelling salesman problem. This is obtained by combining a randomized variant of a rounding algorithm of Bienstock et al. and a primal-dual algorithm of Goemans and Williamson.
Towards a Grid Platform for Scientific Workflows Management
Venue: arXiv cs.DC 2009
Year: 2009

Workflow management systems allow the users to develop complex applications at a higher level, by orchestrating functional components without handling the implementation details. Although a wide range of workflow engines are developed in enterprise environments, the open source engines available for scientific applications lack some functionalities or are too difficult to use for non-specialists. Our purpose is to develop a workflow management platform for distributed systems, that will provide features like an intuitive way to describe workflows, efficient data handling mechanisms and flexible fault tolerance support. We introduce here an architectural model for the workflow platform, based on the ActiveBPEL workflow engine, which we propose to augment with an additional set of components.
Self-similarity properties in a queuing network model
Venue: arXiv cs.NI 2009
Year: 2009

In this paper a model of subscriber telephone network based on the concept of cellular automata is elaborated. Some fractal properties inherent in the model are revealed that vary depending on parameters assigning its operation rules. The main advantage of the model in question is its compatibility with algorithmic methods - a finite set of formal rules, assigned on a finite set of elements (cells), allows precise realization in the form of algorithms.
Prediction of Zoonosis Incidence in Human using Seasonal Auto Regressive Integrated Moving Average (SARIMA)
Venue: arXiv cs.LG 2009
Year: 2009

Zoonosis refers to the transmission of infectious diseases from animal to human. The increasing number of zoonosis incidence makes the great losses to lives, including humans and animals, and also the impact in social economic. It motivates development of a system that can predict the future number of zoonosis occurrences in human. This paper analyses and presents the use of Seasonal Autoregressive Integrated Moving Average (SARIMA) method for developing a forecasting model that able to support and provide prediction number of zoonosis human incidence. The dataset for model development was collected on a time series data of human tuberculosis occurrences in United States which comprises of fourteen years of monthly data obtained from a study published by Centers for Disease Control and Prevention (CDC). Several trial models of SARIMA were compared to obtain the most appropriate model. Then, diagnostic tests were used to determine model validity. The result showed that the SARIMA(9,0,14)(12,1,24)12 is the fittest model. While in the measure of accuracy, the selected model achieved 0.062 of Theils U value. It implied that the model was highly accurate and a close fit. It was also indicated the capability of final model to closely represent and made prediction based on the tuberculosis historical dataset.
BioDiVinE: A Framework for Parallel Analysis of Biological Models
Venue: arXiv cs.CE 2009
Year: 2009

In this paper a novel tool BioDiVinEfor parallel analysis of biological models is presented. The tool allows analysis of biological models specified in terms of a set of chemical reactions. Chemical reactions are transformed into a system of multi-affine differential equations. BioDiVinE employs techniques for finite discrete abstraction of the continuous state space. At that level, parallel analysis algorithms based on model checking are provided. In the paper, the key tool features are described and their application is demonstrated by means of a case study.
On Metric Skyline Processing by PM-tree
Venue: arXiv cs.DB 2009
Year: 2009

The task of similarity search in multimedia databases is usually accomplished by range or k nearest neighbor queries. However, the expressing power of these "single-example" queries fails when the user's delicate query intent is not available as a single example. Recently, the well-known skyline operator was reused in metric similarity search as a "multi-example" query type. When applied on a multi-dimensional database (i.e., on a multi-attribute table), the traditional skyline operator selects all database objects that are not dominated by other objects. The metric skyline query adopts the skyline operator such that the multiple attributes are represented by distances (similarities) to multiple query examples. Hence, we can view the metric skyline as a set of representative database objects which are as similar to all the examples as possible and, simultaneously, are semantically distinct. In this paper we propose a technique of processing the metric skyline query by use of PM-tree, while we show that our technique significantly outperforms the original M-tree based implementation in both time and space costs. In experiments we also evaluate the partial metric skyline processing, where only a controlled number of skyline objects is retrieved.
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
Venue: arXiv cs.LO 2009
Year: 2009

We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have been tested using Isabelle/HOL program extraction facility for inductively defined relations. In particular, the program that computes the Ackermann function type checks and behaves as expected. The main difference (apart from the choice of an Ada-like concrete syntax) with LOOPw comes from the treatment of parameter passing. Indeed, since Ott does not currently fully support alpha-conversion, we rephrased the operational semantics with explicit aliasing in order to implement the out parameter passing mode.
A multiagent urban traffic simulation. Part II: dealing with the extraordinary
Venue: arXiv cs.AI 2009
Year: 2009

In Probabilistic Risk Management, risk is characterized by two quantities: the magnitude (or severity) of the adverse consequences that can potentially result from the given activity or action, and by the likelihood of occurrence of the given adverse consequences. But a risk seldom exists in isolation: chain of consequences must be examined, as the outcome of one risk can increase the likelihood of other risks. Systemic theory must complement classic PRM. Indeed these chains are composed of many different elements, all of which may have a critical importance at many different levels. Furthermore, when urban catastrophes are envisioned, space and time constraints are key determinants of the workings and dynamics of these chains of catastrophes: models must include a correct spatial topology of the studied risk. Finally, literature insists on the importance small events can have on the risk on a greater scale: urban risks management models belong to self-organized criticality theory. We chose multiagent systems to incorporate this property in our model: the behavior of an agent can transform the dynamics of important groups of them.
Can Iterative Decoding for Erasure Correlated Sources be Universal?
Venue: arXiv cs.IT 2009
Year: 2009

In this paper, we consider a few iterative decoding schemes for the joint source-channel coding of correlated sources. Specifically, we consider the joint source-channel coding of two erasure correlated sources with transmission over different erasure channels. Our main interest is in determining whether or not various code ensembles can achieve the capacity region universally over varying channel conditions. We consider two ensembles in the class of low-density generator-matrix (LDGM) codes known as Luby-Transform (LT) codes and one ensemble of low-density parity-check (LDPC) codes. We analyze them using density evolution and show that optimized LT codes can achieve the extremal symmetric point of the capacity region. We also show that LT codes are not universal under iterative decoding for this problem because they cannot simultaneously achieve the extremal symmetric point and a corner point of the capacity region. The sub-universality of iterative decoding is characterized by studying the density evolution for LT codes.
On Improving Local Search for Unsatisfiability
Venue: arXiv cs.AI 2009
Year: 2009

Stochastic local search (SLS) has been an active field of research in the last few years, with new techniques and procedures being developed at an astonishing rate. SLS has been traditionally associated with satisfiability solving, that is, finding a solution for a given problem instance, as its intrinsic nature does not address unsatisfiable problems. Unsatisfiable instances were therefore commonly solved using backtrack search solvers. For this reason, in the late 90s Selman, Kautz and McAllester proposed a challenge to use local search instead to prove unsatisfiability. More recently, two SLS solvers - Ranger and Gunsat - have been developed, which are able to prove unsatisfiability albeit being SLS solvers. In this paper, we first compare Ranger with Gunsat and then propose to improve Ranger performance using some of Gunsat's techniques, namely unit propagation look-ahead and extended resolution.
Adaboost with "Keypoint Presence Features" for Real-Time Vehicle Visual Detection
Venue: arXiv cs.CV 2009
Year: 2009

We present promising results for real-time vehicle visual detection, obtained with adaBoost using new original ?keypoints presence features?. These weak-classifiers produce a boolean response based on presence or absence in the tested image of a ?keypoint? (~ a SURF interest point) with a descriptor sufficiently similar (i.e. within a given distance) to a reference descriptor characterizing the feature. A first experiment was conducted on a public image dataset containing lateral-viewed cars, yielding 95% recall with 95% precision on test set. Moreover, analysis of the positions of adaBoost-selected keypoints show that they correspond to a specific part of the object category (such as ?wheel? or ?side skirt?) and thus have a ?semantic? meaning.