Our initial line of research has shown that, to achieve the best performance on a constraint satisfaction problem, it may be beneficial to translate it to a satisfiability problem. For this translation, it is important to choose both the encoding and satisfiability solver in combination. By doing so, the contrasting performance among solvers on different representations of the same problem can be exploited. In taking these considerations into account, the performance of a solver portfolio augmented with multiple problem transformations can be improved significantly compared to restricting the portfolio to a single problem representation.

Gutierrez and Meseguer show how to enforce consistency during distributed search in the BnB-ADOPT+ algorithm for distributed constraint optimization, but they consider only unconditional deletions. However, during search, more values can be pruned conditionally according to variable instantiations that define subproblems. Enforcing consistency in these subproblems can cause further search space reduction. Here we introduce methods to maintain soft arc consistencies in every subproblem during search. Difficulties lie in the asynchronicity of the algorithm and on the overheads induced by backtracking and undoing. After a careful implementation, experimental results show substantial benefits on several benchmarks.

The problem of finding the set of pareto optimals for constraints and qualitative preferences together is of great interest to many application areas. It can be viewed as a preference constrained optimization problem where the goal is to find one or more feasible solutions that are not dominated by other feasible outcomes. Our work aims to enhance the current literature of the problem by providing solving methods targeting the problem in a dynamic environments. We target the problem with an eye on adopting and benefiting from the current constraint satisfaction techniques.

Satisfiability Modulo Constraint Handling Rules (SMCHR) is the integration of the Constraint Handling Rules (CHRs) solver programming language into a Satisfiability Modulo Theories (SMT) solver framework.  Constraint solvers are implemented in CHR as a set of high-level rules that specify the simplification (rewriting) and constraint propagation behavior.  The traditional CHR execution algorithm manipulates a global store representing a flat conjunction of constraints.  This paper introduces SMCHR: a tight integration of CHR with a modern Boolean Satisfiability (SAT) solver.  Unlike CHR, SMCHR can handle (quantifier-free) formulae with an arbitrary propositional structure.  SMCHR is essentially a Satisfiability Modulo Theories (SMT) solver where the theory T is implemented in CHR.

We target the problem of accuracy and robustness in causal inference from finite data sets. Our aim is to combine the inherent robustness of the Bayesian approach with the theoretical strength and clarity of constraint-based methods. We use a Bayesian score to obtain probability estimates on the input statements used in a constraint-based procedure. These are subsequently processed in decreasing order of reliability, letting more reliable decisions take precedence in case of conflicts, until a single output model is obtained. Tests show that a basic implementation of the resulting Bayesian Constraint-based Causal Discovery (BCCD) algorithm already outperforms established procedures such as FCI and Conservative PC. It indicates which causal decisions in the output have high reliability and which do not. The approach is easily adapted to other application areas such as complex independence tests.

The Extended Global Cardinality Constraint (EGCC) is an important component of constraint solving systems, since it is very widely used to model diverse problems. The literature contains many different versions of this constraint, which trade strength of inference against computational cost. In this paper, I focus on the highest strength of inference usually considered, enforcing generalized arc consistency (GAC) on the target variables. This work is an extensive empirical survey of algorithms and optimizations, considering both GAC on the target variables, and tightening the bounds of the cardinality variables. I evaluate a number of key techniques from the literature, and report important implementation details of those techniques, which have often not been described in published papers. Two new optimizations are proposed for EGCC. One of the novel optimizations (dynamic partitioning, generalized from AllDifferent) was found to speed up search by 5.6 times in the best case and 1.56 times on average, while exploring the same search tree. The empirical work represents by far the most extensive set of experiments on variants of algorithms for EGCC. Overall, the best combination of optimizations gives a mean speedup of 4.11 times compared to the same implementation without the optimizations. This paper is an extended abstract of the publication in Artificial Intelligence [Nightingale, 2011].

We propose a unified approach to plan execution and schedule dispatching that converts a plan, which has been augmented with temporal constraints, into a policy for dispatching. Our approach generalizes the original plan and temporal constraints so that the executor need only consider the subset of state that is relevant to successful execution of valid plan fragments. We can accommodate a variety of calamitous and serendipitous changes to the state of the world by supporting the seamless re-execution or omission of plan fragments, without the need for costly replanning. Our methodology for plan generalization and online dispatching is a novel combination of plan execution and schedule dispatching techniques. We demonstrate the effectiveness of our method through a prototype implementation and a series of experiments.

We introduce MiningZinc, a general framework for constraint-based pattern mining, one of the most popular tasks in data mining. MiningZinc consists of two key components: a language component and a toolchain component. The language allows for high-level and natu- ral modeling of mining problems, such that MiningZinc models closely resemble definitions found in the data mining literature. It is inspired by the Zinc family of languages and systems and supports user-defined constraints and optimization criteria. The toolchain allows for finding solutions to the models. It ensures the solver independence of the language and supports both standard constraint solvers and specialized data mining systems. Au- tomatic model transformations enable the efficient use of different solvers and systems. The combination of both components allows one to rapidly model constraint-based mining problems and execute these with a wide variety of methods. We demonstrate this experimentally for a number of well-known solvers and data mining tasks.

Many formalisms discussed in the literature on qualitative spatial reasoning are designed for expressing static spatial constraints only. However, dynamic situations arise in virtually all applications of these formalisms, which makes it necessary to study variants and extensions involving change. This paper presents a study on the computational complexity of qualitative change. More precisely, we discuss the reasoning task of finding a solution to a temporal sequence of static reasoning problems where this sequence is subject to additional transition constraints. Our focus is primarily on smoothness and continuity constraints: we show how such transitions can be defined as relations and expressed within qualitative constraint formalisms. Our results demonstrate that for point-based constraint formalisms the interesting fragments become NP-completein the presence of continuity constraints, even if the satisfiability problem of its static descriptions is tractable.

Constraint propagation is one of the key techniques in constraint programming, and a large body of work has built up around it. Special-purpose constraint propagation algorithms frequently make implicit use of short supports — by examining a subset of the variables, they can infer support (a justification that a variable-value pair still forms part of a solution to the constraint) for all other variables and values and save substantial work. Recently short supports have been used in general purpose propagators, and (when the constraint is amenable to short supports) speed ups of more than three orders of magnitude have been demonstrated. In this paper we present ShortSTR2, a development of the Simple Tabular Reduction algorithm STR2+. We show that ShortSTR2 is complementary to the existing algorithms ShortGAC and HaggisGAC that exploit short supports, while being much simpler. When a constraint is amenable to short supports, the short support set can be exponentially smaller than the full-length support set. Therefore ShortSTR2 can efficiently propagate many constraints that STR2+ cannot even load into memory. We also show that ShortSTR2 can be combined with a simple algorithm to identify short supports from full-length supports, to provide a superior drop-in replacement for STR2+.