Constraint-Based Reasoning
Experiments with Massively Parallel Constraint Solving
Bordeaux, Lucas (Microsoft Research) | Hamadi, Youssef (Microsoft Research) | Samulowitz, Horst (Microsoft Research)
The computing industry is currently facing a major architectural shift.ย Extra computing power is not coming anymore from higher processor frequencies, but from a growing number of computing cores and processors.ย For AI, and constraint solving in particular, this raises theย question of how to scale current solving techniques to massively parallel architectures. While prior work focusses mostly on small scale parallel constraint solving,ย we conduct the first study on scalability of constraint solving on 100 processors and beyond in this paper. We propose techniques that are simple to apply and show empirically that they scale surprisingly well.ย These techniques establish a performance baseline for parallel constraint solving technologies against which more sophisticated parallel algorithms need toย competeย in the future.
Open Contractible Global Constraints
Maher, Michael (NICTA and UNSW)
Open forms of global constraints allow the addition of new variables to an argument during the execution of a constraint program. ย Such forms are needed for difficult constraint programming problemsย where problem construction and problem solving are interleaved. ย However, in general, filtering that is sound for a global constraint can be unsound whenย the constraint is open. ย This paper provides a simple characterization, called contractibility,ย of the constraints where filtering remains sound when the constraint is open. ย With this characterization we can easily determine whether a constraint is contractible or not. ย In the latter case,ย we can use it to derive the strongest contractible approximation to the constraint. ย We demonstrate how specific algorithms for some closed contractible constraints are easily adapted to open constraints.
A Structural Approach to Reasoning with Quantified Boolean Formulas
Pulina, Luca (Universitร di Genova) | Tacchella, Armando (Universitร di Genova)
In this paper we approach the problem of reasoning with quantified Boolean formulas (QBFs) by combining search and resolution, and by switching between them according to structural properties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolution alone, can be solved by combining them, and that our approach makes a proof-of-concept implementation competitive with current QBF solvers.
Reasoning with Lines in the Euclidean Space
Challita, Khalil Raymond (Holy Spirit University of Kaslik)
The main result of this paper is to show that the problem of instantiating a finite and path-consistent constraint network of lines in the Euclidean space is NP-complete. Indeed, we already know that reasoning with lines in the Euclidean space is NP-hard. In order to prove that this problem is NP-complete, we first establish that a particular instanceย of this problem can be solved by a nondeterministic polynomial-time algorithm, and then we show that solving any finite and path-consistent constraint network of lines in the Euclidean space is at most as difficult as solving that instance.
Towards Efficient Consistency Enforcement for Global Constraints in Weighted Constraint Satisfaction
Lee, Jimmy H. M. (The Chinese University of Hong Kong) | Leung, Ka Lun (The Chinese University of Hong Kong)
Powerful consistency techniques, such as AC* and FDAC*, have been developed for Weighted Constraint Satisfaction Problems (WCSPs) to reduce the space in solution search, but are restricted to only unary and binary constraints.ย On the other hand, van Hoeve et al developed efficient graph-based algorithms for handling soft constraints as classical constraint optimization problems. We prove that naively incorporating van Hoeve's method into the WCSP framework can enforce a strong form of varnothing-Inverse Consistency, which can prune infeasible values and deduce good lower bound estimates.ย We further show how Van Hoeve's method can be modified so as to handle cost projection and extension to maintain the stronger AC* and FDAC* generalized for non-binary constraints.ย Using the soft allDifferent constraint as a testbed, preliminary results demonstrate that our proposal gives improvements up to an order of magnitude both in terms of time and pruning.
Solving Dynamic Constraint Satisfaction Problems by Identifying Stable Features
Wallace, Richard J. (University College Cork) | Grimes, Diarmuid (University College Cork) | Freuder, Eugene C. (University College Cork)
This paper presents a new analysis of dynamic constraint satisfaction problems (DCSPs) with finite domains and a new approach to solving them. We first show that even very small changes in a CSP, in the form of addition of constraints or changes in constraint relations, can have profound effects on search performance. These effects are reflected in the amenability of the problem to different forms of heuristic action as well as overall quality of search. In addition, classical DCSP methods perform poorly on these problems because there are sometimes no solutions similar to the original one found. We then show that the same changes do not markedly affect the locations of the major sources of contention in the problem. A technique for iterated sampling that performs a careful assessment of this property and uses the information during subsequent search, performs well even when it only uses information based on the original problem in the DCSP sequence. The result is a new approach to solving DCSPs that is based on a robust strategy for ordering variables rather than on robust solutions.
On Combinations of Binary Qualitative Constraint Calculi
Woelfl, Stefan (University of Freiburg) | Westphal, Matthias (University of Freiburg)
Qualitative constraint calculi are representation formalisms that allow for efficient reasoning about spatial and temporal information. Many of the calculi discussed in the field of Qualitative Spatial and Temporal Reasoning can be defined as combinations of other, simpler and more compact formalisms. On the other hand, existing calculi can be combined to a new formalism in which one can represent, and reason about, different aspects of a domain at the same time. For example, Gerevini and Renz presented a loose combination of the region connection calculus RCC-8 and the point algebra: the resulting formalism integrates topological and qualitative size relations between spatially extended objects. In this paper we compare the approach by Gerevini and Renz to a method that generates a new qualitative calculus by exploiting the semantic interdependencies between the component calculi. We will compare these two methods and analyze some formal relationships between a combined calculus and its components. The paper is completed by an empirical case study in which the reasoning performance of the suggested methods is compared on random test instances.
Hiding Quiet Solutions in Random Constraint Satisfaction Problems
Krzakala, Florent, Zdeborovรก, Lenka
We study constraint satisfaction problems on the so-called 'planted' random ensemble. We show that for a certain class of problems, e.g. graph coloring, many of the properties of the usual random ensemble are quantitatively identical in the planted random ensemble. We study the structural phase transitions, and the easy/hard/easy pattern in the average computational complexity. We also discuss the finite temperature phase diagram, finding a close connection with the liquid/glass/solid phenomenology.
Circuit Complexity and Decompositions of Global Constraints
Bessiere, Christian, Katsirelos, George, Narodytska, Nina, Walsh, Toby
We show that tools from circuit complexity can be used to study decompositions of global constraints. In particular, we study decompositions of global constraints into conjunctive normal form with the property that unit propagation on the decomposition enforces the same level of consistency as a specialized propagation algorithm. We prove that a constraint propagator has a a polynomial size decomposition if and only if it can be computed by a polynomial size monotone Boolean circuit. Lower bounds on the size of monotone Boolean circuits thus translate to lower bounds on the size of decompositions of global constraints. For instance, we prove that there is no polynomial sized decomposition of the domain consistency propagator for the ALLDIFFERENT constraint.
Decompositions of All Different, Global Cardinality and Related Constraints
Bessiere, Christian, Katsirelos, George, Narodytska, Nina, Quimper, Claude-Guy, Walsh, Toby
We show that some common and important global constraints like ALL-DIFFERENT and GCC can be decomposed into simple arithmetic constraints on which we achieve bound or range consistency, and in some cases even greater pruning. These decompositions can be easily added to new solvers. They also provide other constraints with access to the state of the propagator by sharing of variables. Such sharing can be used to improve propagation between constraints. We report experiments with our decomposition in a pseudo-Boolean solver.