A wide range of problems can be modelled as constraint satisfaction problems (CSPs), that is, a set of constraints that must be satisfied simultaneously. Constraints can either be represented extensionally, by explicitly listing allowed combinations of values, or implicitly, by special-purpose algorithms provided by a solver. Such implicitly represented constraints, known as global constraints, are widely used; indeed, they are one of the key reasons for the success of constraint programming in solving real-world problems. In recent years, a variety of restrictions on the structure of CSP instances that yield tractable classes have been identified. However, many such restrictions fail to guarantee tractability for CSPs with global constraints. In this paper, we investigate the properties of extensionally represented constraints that these restrictions exploit to achieve tractability, and show that there are large classes of global constraints that also possess these properties. This allows us to lift these restrictions to the global case, and identify new tractable classes of CSPs with global constraints.

This paper provides a broad overview of the situation in Parallel SAT Solving. A set of challenges to researchers is presented which, we believe, must be met to ensure the practical applicability of Parallel SAT Solvers in the future. All these challenges are described informally, but put into perspective with related research results, and a (subjective) grading of difficulty for each of them is provided.

In this paper, we present fast polynomial-time algorithms for solving classes of submodular constraints over Boolean domains. We pose the identified classes of problems within the general framework of Weighted Constraint Satisfaction Problems (WCSPs), reformulated as minimum weighted vertex cover problems. We examine the Constraint Composite Graphs (CCGs) associated with these WCSPs and provide simple arguments for establishing their tractability. We construct simple - almost trivial - bipartite graph representations for submodular cost functions, and reformulate these WCSPs as max-flow problems on bipartite graphs. By doing this, we achieve better time complexities than state-of-the-art algorithms. We also use CCGs to exploit planarity in variable interaction graphs, and provide algorithms with significantly improved time complexities for classes of submodular constraints. Moreover, our framework for exploiting planarity is not limited to submodular constraints. Our work confirms the usefulness of studying CCGs associated with combinatorial problems modeled as WCSPs.

In this paper, we present an efficient algorithm for verifying path-consistency on a binary constraint network. The complexities of our algorithm beat the previous conjectures on the lower bounds for verifying path-consistency. We therefore defeat the proofs for several published results that incorrectly rely on these conjectures. Our algorithm is motivated by the idea of reformulating path-consistency verification as fast matrix multiplication. Further, for a computational model that counts arithmetic operations (rather than bit operations), a clever use of the properties of prime numbers allows us to design an even faster variant of the algorithm. Based on our algorithm, we hope to inspire a new class of techniques for verifying and even establishing varying levels of local-consistency on given constraint networks.

Many real-world applications require the successful combination of spatial and temporal reasoning. In this paper, we study the general framework of the Traveling Salesman Problem with Simple Temporal Constraints. Representationally, this framework subsumes the Traveling Salesman Problem, Simple Temporal Problems, as well as many of the frameworks described in the literature. We analyze the theoretical properties of the combined problem providing strong inapproximability results for the general problem, and positive results for some special cases.

Many works have studied the properties of CSPs which are based on the structures of constraint networks, or based on the features of compatibility relations. Studies on structures rely generally on properties of graphs for binary CSPs and on properties of hypergraphs for the general case, that is CSPs with constraints of arbitrary arity. In the second case, using the dual representation of hypergraphs, that is a reformulation of the instances, we can exploit notions and properties of graphs. For the studies of compatibility relations, the exploitation of properties of graphs is possible studying a graph called microstructure which allows to reformulate instances of binary CSP. Unfortunately, this approach is limited to CSPs with binary constraints. In this paper, we propose theoretical tools based on graphs to represent microstructures for the general case. This approach avoids to exploit directly hypergraphs, even if the microstructure based on hypergraphs has already been mentioned in (Cohen 2003). The advantage of such an approach is that the literature of Graph Theory is really more extended than one of Hypergraph Theory. Thus the theoretical results and efficient algorithms are more numerous, offering a larger number of existing tools which can be operated. We introduce here three possible definitions of microstructures based on graphs. We show how these representations can form new theoretical tools to generalize a number of results already obtained on binary CSPs. We think that these representations should be of interest for the community, firstly for the generalization of existing results, but also to obtain original results for CSPs with constraints of arbitrary arity.

Unlike mathematical programming and SAT solving, ConstraintProgramming (CP) is based on the idea that both modeling and solving of combinatorial optimization problems can be based on conjunctions of loosely coupled, recurring, combinatorial sub-problems (aka "global constraints"). This rich representational approach means that, for better or for worse, pretty much anything can be expressed as a global constraint. Much of CP's success, however, has come from exploiting only one aspect of the rich constraint definition: global constraint propagation. In this talk, I will investigate how work in CP, SAT, AI planning, and mathematical programming can be understood as more seriously pursuing the implications of a rich constraint definition and how the interplay between local and global information can lead to dynamic problem reformulations and a flexible hybrid solver architecture.

There has been a tremendous advance in domain-independent planning over the past decades, and planners have become increasingly efficient at finding plans. However, this has not been paired by any corresponding improvement in detecting unsolvable instances. Such instances are obviously important but largely neglected in planning. In other areas, such as constraint solving and model checking, much effort has been spent on devising methods for detecting unsolvability. We introduce a method for detecting unsolvable planning instances that is loosely based on consistency checking in constraint programming. Our method balances completeness against efficiency through a parameter k: the algorithm identifies more unsolvable instances but takes more time for increasing values of k. We present empirical data for our algorithm and some standard planners on a number of unsolvable instances, demonstrating that our method can be very efficient where the planners fail to detect unsolvability within reasonable resource bounds. We observe that planners based on the h^m heuristic or pattern databases are better than other planners for detecting unsolvability. This is not a coincidence since there are similarities (but also significant differences) between our algorithm and these two heuristic methods.

This paper provides a broad overview of the situation in Parallel SAT Solving. A set of challenges to researchers is presented which, we believe, must be met to ensure the practical applicability of Parallel SAT Solvers in the future. All these challenges are described informally, but put into perspective with related research results, and a (subjective) grading of difficulty for each of them is provided.

We can break symmetry by eliminating solutions within each symmetry class. For instance, the Lex-Leader method eliminates all but the smallest solution in the lexicographical ordering. Unfortunately, the Lex-Leader method is intractable in general. We prove that, under modest assumptions, we cannot reduce the worst case complexity of breaking symmetry by using other orderings on solutions. We also prove that a common type of symmetry, where rows and columns in a matrix of decision variables are interchangeable, is intractable to break when we use two promising alternatives to the lexicographical ordering: the Gray code ordering (which uses a different ordering on solutions), and the Snake-Lex ordering (which is a variant of the lexicographical ordering that re-orders the variables). Nevertheless, we show experimentally that using other orderings like the Gray code to break symmetry can be beneficial in practice as they may better align with the objective function and branching heuristic.