Making constraint solvers more usable: overconstraint problem

The richness and expressive power of geometric constraints causes unintended ambiguities and inconsistencies during their solution or realization. For example, geometric constraint problems may turn out to be overconstrained requiring the user to delete one or more of the input constraints, and the solutions must then be dynamically updated. Without proper guidance by the constraint solver, the user must have profound insight into the mathematical nature of constraint systems and understand the internals of the solver algorithm. But a general user is most likely unfamiliar with those problems, so that the required interaction with the constraint solver may well be beyond the user's ability. In this paper, we present strategies and techniques to empower the user to deal effectively with the overconstraint problem while not requiring him or her to become an expert in the mathematics of constraint solving.We formulate this problem as a series of formal requirements that gel with other essentials of constraint solvers. We then give algorithmic solutions that are both general and efficient (running time typically linear in the number of relevant constraints).     

Engineering constraint solvers for automatic analysis of probabilistic hybrid automata

In this article, we recall different approaches to the constraint-based, symbolic analysis of hybrid discrete-continuous systems and combine them to a technology able to address hybrid systems exhibiting both non-deterministic and probabilistic behavior akin to infinite-state Markov decision processes. To enable mechanized analysis of such systems, we extend the reasoning power of arithmetic satisfiability-modulo-theories (SMT) solving by, first, reasoning over ordinary differential equations (ODEs) and, second, a comprehensive treatment of randomized (also known as stochastic) quantification over discrete variables as well as existential quantification over both discrete and continuous variables within the mixed Boolean-arithmetic constraint system. This provides the technological basis for a constraint-based analysis of dense-time probabilistic hybrid automata, extending previous results addressing discrete-time automata [33]. Generalizing SMT-based bounded model-checking of hybrid automata [5], [31], stochastic SMT including ODEs permits the direct analysis of probabilistic bounded reachability problems of dense-time probabilistic hybrid automata without resorting to approximation by intermediate finite-state abstractions.     

Handwritten digit segmentation: a comparative study

In this work, algorithms for segmenting handwritten digits based on different concepts are compared by evaluating them under the same conditions of implementation. A robust experimental protocol based on a large synthetic database is used to assess each algorithm in terms of correct segmentation and computational time. Results on a real database are also presented. In addition to the overall performance of each algorithm, we show the performance for different types of connections, which provides an interesting categorization of each algorithm. Another contribution of this work concerns the complementarity of the algorithms. We have observed that each method is able to segment samples that cannot be segmented by any other method, and do so independently of their individual performance. Based on this observation, we conclude that combining different segmentation algorithms may be an appropriate strategy for improving the correct segmentation rate.     

Planar fiducial markers: a comparative study

Virtual Reality - Fiducial markers are a cost-effective solution for solving labeling and monocular localization problems, making them valuable tools for augmented reality (AR), robot navigation,...     

Speaker distinguishing distances: a comparative study

Speaker discrimination is a vital aspect of speaker recognition applications such as speaker identification, verification, clustering, indexing and change-point detection. These tasks are usually performed using distance-based approaches to compare speaker models or features from homogeneous speaker segments in order to determine whether or not they belong to the same speaker. Several distance measures and features have been examined for all the different applications, however, no single distance or feature has been reported to perform optimally for all applications in all conditions. In this paper, a thorough analysis is made to determine the behavior of some frequently used distance measures, as well as features, in distinguishing speakers for different data lengths. Measures studied include the Mahalanobis distance, Kullback-Leibler (KL) distance, T ² statistic, Hellinger distance, Bhattacharyya distance, Generalized Likelihood Ratio (GLR), Levenne distance, L ₂ and L _∞ distances. The Mel-Scale Frequency Cepstral Coefficient (MFCC), Linear Predictive Cepstral Coefficients (LPCC), Line Spectral Pairs (LSP) and the Log Area Ratios (LAR) comprise the features investigated. The usefulness of these measures is studied for different data lengths. Generally, a larger data size for each speaker results in better speaker differentiating capability, as more information can be taken into account. However, in some applications such as segmentation of telephone data, speakers change frequently, making it impossible to obtain large speaker-consistent utterances (especially when speaker change-points are unknown). A metric is defined for determining the probability of speaker discrimination error obtainable for each distance measure using each feature set, and the effect of data size on this probability is observed. Furthermore, simple distance-based speaker identification and clustering systems are developed, and the performances of each distance and feature for various data sizes are evaluated on these systems in order to illustrate the importance of choosing the appropriate distance and feature for each application. Results show that for tasks which do not involve any limitation of data length, such as speaker identification, the Kullback Leibler distance with the MFCCs yield the highest speaker differentiation performance, which is comparable to results obtained using more complex state-of-the-art speaker identification systems. Results also indicate that the Hellinger and Bhattacharyya distances with the LSPs yield the best performance for small data sizes.     

Meta-Level interpretation of constraint languages a case study: Logical primitives

This paper provides a detailed presentation of a Prolog-written meta-level interpreter for a constraint logic programming (CLP) language for expressing equalities and disequalities of finite trees, as well as non-negative integers (arities). The logical interpretation of the Prolog primitive functor (whose arguments are trees and arity) is used to illustrate the interactions among constraints pertaining to multiple domains. The paper’s objective is to provide insights about CLP language design and to present a modularized, incrementally-expandable meta-processor for this class of languages.     

Verifying a signature architecture: a comparative case study

We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises several concurrently executing systems that authenticate users and generate and store digital signatures by passing security relevant data through a tightly controlled interface. The architecture is interesting from a formal-methods perspective as it involves complex operations on data as well as process coordination and hence is a candidate for both data-oriented and process-oriented formal methods. We have built and verified two models of the signature architecture using two representative formal methods. In the first, we specify a data model of the architecture in Z that we extend to a trace model and interactively verify by theorem proving. In the second, we model the architecture as a system of communicating processes that we verify by finite-state model checking. We provide a detailed comparison of these two different approaches to formalization (infinite state with rich data types versus finite state) and verification (theorem proving versus model checking). Contrary to common belief, our case study suggests that Z is well suited for temporal reasoning about process models with complex operations on data. Moreover, our comparison highlights the advantages of proving theorems about such models and provides evidence that, in the hands of an experienced user, theorem proving may be neither substantially more time-consuming nor more complex than model checking.     

Extending SMT solvers with support for finite domain <Literal>alldifferent</Literal> constraint

In this paper we consider integration of SMT solvers with the filtering algorithms for the finite domain alldifferent constraint. Such integration makes SMT solvers suitable for solving constraint satisfaction problems with the alldifferent constraint involved. First, we present a novel algorithm for explaining inconsistencies and propagations in the alldifferent constraint. We compare it to Katsirelos’ algorithm and flow-based algorithms that are commonly used for that purpose. Then we describe our DPLL(T)-compliant SMT theory solver for constraint satisfaction problems that include alldifferent constraints. We also provide an experimental evaluation of our approach.     

Generative model-based document clustering: a comparative study

This paper presents a detailed empirical study of 12 generative approaches to text clustering, obtained by applying four types of document-to-cluster assignment strategies (hard, stochastic, soft and deterministic annealing (DA) based assignments) to each of three base models, namely mixtures of multivariate Bernoulli, multinomial, and von Mises-Fisher (vMF) distributions. A large variety of text collections, both with and without feature selection, are used for the study, which yields several insights, including (a) showing situations wherein the vMF-centric approaches, which are based on directional statistics, fare better than multinomial model-based methods, and (b) quantifying the trade-off between increased performance of the soft and DA assignments and their increased computational demands. We also compare all the model-based algorithms with two state-of-the-art discriminative approaches to document clustering based, respectively, on graph partitioning (CLUTO) and a spectral coclustering method. Overall, DA and CLUTO perform the best but are also the most computationally expensive. The vMF models provide good performance at low cost while the spectral coclustering algorithm fares worse than vMF-based methods for a majority of the datasets.     

Filtering for texture classification: a comparative study

In this paper, we review most major filtering approaches to texture feature extraction and perform a comparative study. Filtering approaches included are Laws masks (1980), ring/wedge filters, dyadic Gabor filter banks, wavelet transforms, wavelet packets and wavelet frames, quadrature mirror filters, discrete cosine transform, eigenfilters, optimized Gabor filters, linear predictors, and optimized finite impulse response filters. The features are computed as the local energy of the filter responses. The effect of the filtering is highlighted, keeping the local energy function and the classification algorithm identical for most approaches. For reference, comparisons with two classical nonfiltering approaches, co-occurrence (statistical) and autoregressive (model based) features, are given. We present a ranking of the tested approaches based on extensive experiments     

Compressed-domain visual saliency models: a comparative study

Computational modeling of visual saliency has become an important research problem in recent years, with applications in video quality estimation, video compression, object tracking, retargeting, summarization, and so on. While most visual saliency models for dynamic scenes operate on raw video, several models have been developed for use with compressed-domain information such as motion vectors and transform coefficients. This paper presents a comparative study of eleven such models as well as two high-performing pixel-domain saliency models on two eye-tracking datasets using several comparison metrics. The results indicate that highly accurate saliency estimation is possible based only on a partially decoded video bitstream. The strategies that have shown success in compressed-domain saliency modeling are highlighted, and certain challenges are identified as potential avenues for further improvement.

     

Factors affecting participation of solvers in crowdsourcing: an empirical study from China

Crowdsourcing comprises a variety of creative contests, and its success is closely related to the quantity and quality of solvers. The research model of factors influencing the quantity and quality of solvers with respect to contest arrangement attributes and market competition situation has been developed in this paper, and the model has been tested with data from a crowdsourcing website in China. The results show that higher awards, easier tasks, longer duration and lower competition intensity lead to a higher number of solvers. Higher awards, longer duration and higher difficulty level of tasks lead to higher ability level of winners, but competition intensity and market price for other competing projects do not show significant correlation with the ability level of winners.     

Consul: a parallel constraint language

The author describes a constraint-based language, Consul, that can exploit implicit parallelism. The results are reported of the first stage of the Consul project, which was designed to produce empirical evidence for or against Consul as a parallel language. To produce the evidence, a parallel-execution model is developed that is based on local propagation and uses some important generalizations of earlier work on local propagation. A set of tools was developed to measure the execution of several Consul programs. The results suggest that considerable parallelism is available in Consul programs and that local propagation is a viable mechanism for solving most real-world constraints. The Consul programs demonstrate that programmers can control performance through the proper choice of algorithms, despite Consul's declarative nature     

RETRACTED: Shortest paths in a lattice network: a comparative study

This article has been retracted at the request of the editor.Reason: The article published in Volume 28, issue 11, pages 1131–1139 was retracted as subsequent to publication it was found to be substantially the same as Shortest Paths with Euclidean Distances: An Explanatory Model, by B L Golden and M Ball, published in Networks, Volume 8 (1978), pages 297–314.We apologise to Professor B L Golden and Professor M Ball for not discovering this instance of plagiarism prior to publication.This Notice was published in CAOR, Volume 29, Issue 7 (June 2002).     

Micro-differential evolution: Diversity enhancement and a comparative study

Differential evolution (DE) algorithm suffers from high computational time due to slow nature of evaluation. Micro-DE (MDE) algorithms utilize a very small population size, which can converge faster to a reasonable solution. Such algorithms are vulnerable to premature convergence and high risk of stagnation. This paper proposes a MDE algorithm with vectorized random mutation factor (MDEVM), which utilizes the small size population benefit while empowers the exploration ability of mutation factor through randomizing it in the decision variable level. The idea is supported by analyzing mutation factor using Monte-Carlo based simulations. To facilitate the usage of MDE algorithms with very-small population sizes, a new mutation scheme for population sizes less than four is also proposed. Furthermore, comprehensive comparative simulations and analysis on performance of the MDE algorithms over various mutation schemes, population sizes, problem types (i.e. uni-modal, multi-modal, and composite), problem dimensionalities, and mutation factor ranges are conducted by considering population diversity analysis for stagnation and pre-mature convergence. The MDEVM is implemented using a population-based parallel model and studies are conducted on 28 benchmark functions provided for the IEEE CEC-2013 competition. Experimental results demonstrate high performance in convergence speed of the proposed MDEVM algorithm.     

Non-stationary iterative solvers on a PC cluster

In this study, we introduce cost effective strategies and algorithms for parallelizing the Krylov subspace based non-stationary iterative solvers such as Bi-CGM and Bi-CGSTAB for distributed computing on a cluster of PCs using ANULIB message passing libraries. We investigate the effectiveness of the parallel solvers on the linear systems resulting in numerical solution of some 2D and 3D nonlinear partial differential equations governing heat convection process by finite element, finite difference and wavelet based numerical schemes. Largely Bi-CGM is found to give better performance measured in terms of speedup factors.     

Methods for constraint violation suppression in the numerical simulation of constrained multibody systems – A comparative study

Multibody systems are frequently modeled as constrained systems, and the arising governing equations incorporate the closing constraint equations at the acceleration level. One consequence of accumulation of integration truncation errors is the phenomenon of violation of the lower-order constraint equations by the numerical solutions to the governing equations. The constraint drift usually tends to increase in time and may spoil reliability of the simulation results. In this paper a comparative study of three methods for constraint violation suppression is presented: the popular Baumgarte’s constraint violation stabilization method, a projective scheme for constraint violation elimination, and a novel scheme patterned after that proposed recently by Braun and Goldfarb [D.J. Braun, M. Goldfarb, Eliminating constraint drift in the numerical simulation of constrained dynamical systems, Comput. Meth. Appl. Mech. Engrg., 198 (2009) 3151–3160]. The methods are confronted with respect to simplicity in applications, numerical effectiveness and influence on accuracy of the constraint-consistent motion.     

VERICOMP: a system to compare and assess verified IVP solvers

Obtaining verified numerical solutions to initial value problems (IVPs) for ordinary differential equations (ODEs) is important in many application areas (e.g. biomechanics or automatic control). During the last decades, a number of solvers have been developed for this purpose. However, they are rarely used by industry engineers. One reason for this is the lack of information about what tool with what settings to choose. Therefore, it is necessary to develop a system for testing the available tools and recommending an ODE solver best suited for the task at hand in the area of verified software. In this paper, we present the first version of our web-based platform VERICOMP for assessing verified IVP solvers. We discuss a possible classification for user problems, suitable comparison criteria and measures for the quantification of overestimation. After that, we introduce the platform itself, which allows us to compare different solvers on a problem class or to evaluate the performance of a single solver on different problem classes. In addition, we describe how to extend VERICOMP with a recommender system that automatically suggests the most suitable solver based on user preferences and solver statistics.     

Automatically configuring constraint satisfaction programs: A case study

Multi-tac is a learning system that synthesizes heuristic constraint satisfaction programs. The system takes a library of generic algorithms and heuristics and specializes them for a particular application. We present a detailed case study with three different distributions of a single combinatorial problem, Minimum Maximal Matching, and show that Muti-tac can synthesize programs for these different distributions that perform on par with hand-coded programs and that exceed the performance of some well-known satisfiability algorithms. In synthesizing a program, Multi-tac bases its choice of heuristics on an instance distribution, and we demonstrate that this capability has a significant impact on the results.