Constraint-Based Reasoning
Automated Regression Testing Using Constraint Programming
Gotlieb, Arnaud (Simula Research Laboratory) | Carlsson, Mats (Swedish Institute in Computer Science) | Liaeen, Marius (CISCO Systems) | Marijan, Dusica (Simula Research Laboratory) | Petillon, Alexandre (Simula Research Laboratory)
In software validation, regression testing aims to check the absence of regression faults in new releases of a software system. Typically, test cases used in regression testing are executed during a limited amount of time and are selected to check a given set of user requirements. When testing large systems, the number of regression tests grows quickly over the years, and yet the available time slot stays limited. In order to overcome this problem, an approach known as test suite reduction (TSR), has been developed in software engineering to select a smallest subset of test cases, so that each requirement remains covered at least once. However solving the TSR problem is difficult as the underlying optimization problem is NP-hard, but it is also crucial for vendors interested in reducing the time to market of new software releases. In this paper, we address regression testing and TSR with Constraint Programming (CP). More specifically, we propose new CP models to solve TSR that exploit global constraints, namely NValue and GCC. We reuse a set of preprocessing rules to reduce a priori each instance, and we introduce a structure-aware search heuristic. We evaluated our CP models and proposed improvements against existing approaches, including a simple greedy approach and MINTS, the state-of-the-art tool of the software engineering community. Our experiments show that CP outperforms both the greedy approach and MINTS when it is interfaced with MiniSAT, in terms of percentage of reduction and execution time. When MINTS is interfaced with CPLEX, we show that our CP model performs better only on percentage of reduction. Finally, by working closely with validation engineers from Cisco Systems, Norway, we integrated our CP model into an industrial regression testing process.
Fuzzy Maximum Satisfiability
Halaby, Mohamed El, Abdalla, Areeg
In this paper, we extend the Maximum Satisfiability (MaxSAT) problem to {\L}ukasiewicz logic. The MaxSAT problem for a set of formulae {\Phi} is the problem of finding an assignment to the variables in {\Phi} that satisfies the maximum number of formulae. Three possible solutions (encodings) are proposed to the new problem: (1) Disjunctive Linear Relations (DLRs), (2) Mixed Integer Linear Programming (MILP) and (3) Weighted Constraint Satisfaction Problem (WCSP). Like its Boolean counterpart, the extended fuzzy MaxSAT will have numerous applications in optimization problems that involve vagueness.
Representing and Reasoning with Qualitative Preferences: Tools and Applications
Santhanam, Ganesh Ram, Basu, Samik, Honavar, Vasant
This book provides a tutorial introduction to modern techniques for representing and reasoning about qualitative preferences with respect to a set of alternatives. The syntax and semantics of several languages for representing preference languages, including CP-nets, TCP-nets, CI-nets, and CP-theories, are reviewed. Some key problems in reasoning about preferences are introduced, including determining whether one alternative is preferred to another, or whether they are equivalent, with respect to a given set of preferences. These tasks can be reduced to model checking in temporal logic. Specifically, an induced preference graph that represents a given set of preferences can be efficiently encoded using a Kripke Structure for Computational Tree Logic (CTL).
Lifted Inference Rules With Constraints
Mittal, Happy, Mahajan, Anuj, Gogate, Vibhav G., Singla, Parag
Lifted inference rules exploit symmetries for fast reasoning in statistical relational models.Computational complexity of these rules is highly dependent on the choice of the constraint language they operate on and therefore coming up with the right kind of representation is critical to the success of lifted inference. In this paper, we propose a new constraint language, called setineq, which allows subset, equality and inequality constraints, to represent substitutions over the variables inthe theory. Our constraint formulation is strictly more expressive than existing representations, yet easy to operate on. We reformulate the three main lifting rules: decomposer, generalized binomial and the recently proposed single occurrence for MAP inference, to work with our constraint representation. Experiments onbenchmark MLNs for exact and sampling based inference demonstrate the effectiveness of our approach over several other existing techniques.
Subsampled Power Iteration: a Unified Algorithm for Block Models and Planted CSP's
Feldman, Vitaly, Perkins, Will, Vempala, Santosh
We present an algorithm for recovering planted solutions in two well-known models, the stochastic block model and planted constraint satisfaction problems (CSP), via a common generalization in terms of random bipartite graphs. Our algorithm matches up to a constant factor the best-known bounds for the number of edges (or constraints) needed for perfect recovery and its running time is linear in the number of edges used. The time complexity is significantly better than both spectral and SDP-based approaches.The main contribution of the algorithm is in the case of unequal sizes in the bipartition that arises in our reduction from the planted CSP. Here our algorithm succeeds at a significantly lower density than the spectral approaches, surpassing a barrier based on the spectral norm of a random matrix.Other significant features of the algorithm and analysis include (i) the critical use of power iteration with subsampling, which might be of independent interest; its analysis requires keeping track of multiple norms of an evolving solution (ii) the algorithm can be implemented statistically, i.e., with very limited access to the input distribution (iii) the algorithm is extremely simple to implement and runs in linear time, and thus is practical even for very large instances.
Lifted Symmetry Detection and Breaking for MAP Inference
Kopp, Timothy, Singla, Parag, Kautz, Henry
Symmetry breaking is a technique for speeding up propositional satisfiability testing by adding constraints to the theory that restrict the search space while preserving satisfiability. In this work, we extend symmetry breaking to the problem of model finding in weighted and unweighted relational theories, a class of problems that includes MAP inference in Markov Logic and similar statistical-relational languages. We introduce term symmetries, which are induced by an evidence set and extend to symmetries over a relational theory. We provide the important special case of term equivalent symmetries, showing that such symmetries can be found in low-degree polynomial time. We show how to break an exponential number of these symmetries with added constraints whose number is linear in the size of the domain. We demonstrate the effectiveness of these techniques through experiments in two relational domains. We also discuss the connections between relational symmetry breaking and work on lifted inference in statistical-relational reasoning.
Relations Between Spatial Calculi About Directions and Orientations
Mossakowski, Till, Moratz, Reinhard
Qualitative spatial descriptions characterize essential properties of spatial objects or configurations by relying on relative comparisons rather than measuring. Typically, in qualitative approaches only relatively coarse distinctions between configurations are made. Qualitative spatial knowledge can be used to represent incomplete and underdetermined knowledge in a systematic way. This is especially useful if the task is to describe features of classes of configurations rather than individual configurations. Although reasoning with them is generally NP-hard (even IR-complete), relative directions are important because they play a key role in human spatial descriptions and there are several approaches how to represent them using qualitative methods. In these approaches directions between spatial locations can be expressed as constraints over infinite domains, e.g. the Euclidean plane. The theory of relation algebras has been successfully applied to this field. Viewing relation algebras as universal algebras and applying and modifying standard tools from universal algebra in this work, we (re)define notions of qualitative constraint calculus, of homomorphism between calculi, and of quotient of calculi.Based on this method we derive important properties for spatial calculi from corresponding properties of related calculi. From a conceptual point of view these formal mappings between calculi are a means to translate between different granularities.
Robustness and Flexibility of GHOST
Fradin, Julien (UniversitƩ de Nantes) | Richoux, Florian (UniversitƩ de Nantes)
GHOST is a framework to help game developers to model and implement their own optimization problems, or to simply instantiate a problem already encoded in GHOST. Previous works show that GHOST leads to high-quality solutions in some tens of milliseconds for three RTS-related problems: build order, wall-in placementĀ and target selection. In this paper, we show the robustness of the framework, having very good results for a problem it is not designed for (pathfinding), as well as its flexibility, where it is easy to propose different models of the same problem (resource allocation problem). The goal of the paper is not to improve the state-of-the-art on these problems, but to use them as benchmarks to test GHOST properties.
Transalg: a Tool for Translating Procedural Descriptions of Discrete Functions to SAT
Otpuschennikov, Ilya, Semenov, Alexander, Kochemazov, Stepan
Many new methods for solving Boolean Satisfiability Problem (SAT) were introduced in the past two decades. These methods make it possible to solve combinatorial problems from various areas [2]. One can use different approaches to encode an original problem to SAT [14]. Often each particular problem requires researchers to develop and implement special encoding technique. Recently a number of systems that automate procedures of encoding combinatorial problems to SAT were developed [6,7,12,17,20].
ParallelPC: an R package for efficient constraint based causal exploration
Le, Thuc Duy, Hoang, Tao, Li, Jiuyong, Liu, Lin, Hu, Shu
Discovering causal relationships from data is the ultimate goal of many research areas. Constraint based causal exploration algorithms, such as PC, FCI, RFCI, PC-simple, IDA and Joint-IDA have achieved significant progress and have many applications. A common problem with these methods is the high computational complexity, which hinders their applications in real world high dimensional datasets, e.g gene expression datasets. In this paper, we present an R package, ParallelPC, that includes the parallelised versions of these causal exploration algorithms. The parallelised algorithms help speed up the procedure of experimenting big datasets and reduce the memory used when running the algorithms. The package is not only suitable for super-computers or clusters, but also convenient for researchers using personal computers with multi core CPUs. Our experiment results on real world datasets show that using the parallelised algorithms it is now practical to explore causal relationships in high dimensional datasets with thousands of variables in a single multicore computer. ParallelPC is available in CRAN repository at https://cran.rproject.org/web/packages/ParallelPC/index.html.