Program

Graphical models, also known as Markov/Gibbs random fields, are structured statistical models with many applications in computer vision, machine learning, natural language processing, bioinformatics, and other disciplines. The field underwent a revolution in the last two decades (though nowadays overshadowed by the deep learning revolution), enabled mainly by the advent of new inference algorithms. Graphical models are similar to constraint systems, in particular maximum a-posteriori (MAP) inference in graphical models corresponds to constraint satisfaction+optimization. The tutorial will compare graphical models and constraint systems, focusing on similarities and differences in their definitions, tasks attached to them, and typical data. Then it will survey seminal results of the graphical model community that might be inspiring for constraint satisfaction+optimization researchers, mainly focusing on MAP inference. We hope that the tutorial will narrow the multidiscplinary gap between the two communities.

This tutorial introduces the inner workings of PicatSAT, a SAT-based CSP solver available in Picat that won prizes in the XCSP competition and the MiniZinc Challenge in 2018. PicatSAT adopts the sign-and-magnitude log-encoding for domain variables, which had been perceived to be a bad idea due to its lack of propagation strengths, despite its compactness. Log-encoding for constraints resembles the binary representation of numbers used in computer hardware, and many algorithms and optimization opportunities have been exploited by hardware design systems. PicatSAT adopts some optimizations from CP systems, language compilers, and hardware design systems for encoding arithmetic constraints into compact and efficient SAT code: it preprocesses constraints before compilation in order to remove no-good values from the domains of variables whenever possible; it eliminates common subexpressions so that no primitive constraint is duplicated; it uses a logic optimizer to generate optimized code for small constraints. PicatSAT also incorporates an optimization, named equivalence reasoning, which identifies values or equivalence relationships of Boolean variables in primitive arithmetic constraints. These optimizations significantly improve the quality of the generated code. Global constraints, including table constraints, constitute an essential part of constraint programming. They not only allow easy modeling of many combinatorial problems, but also enable use of powerful propagation algorithms. A global constraint can be decomposed into primitive constraints in many different ways, and the quality of the decomposed code tends to be dependent on the encoding of domain variables. This tutorial also presents PicatSAT's decomposers for some of the basic global constraints, including all_different, table, element, regular, circuit, and cumulative.

CP Optimizer is a generic system, largely based on CP, to model and solve real-world combinatorial optimization problems with a particular focus on planning and scheduling applications. It provides an algebraic language with simple mathematical concepts (such as intervals, sequences or functions) to capture the temporal dimension of planning and scheduling problems in a combinatorial optimization framework. CP Optimizer implements a model-and-run paradigm that vastly reduces the burden on the user to understand CP or scheduling algorithms: modeling is by far the most important. The automatic search integrates a large panel of techniques from Artificial Intelligence (constraint programming, temporal reasoning, learning, ...) and Operations Research (mathematical programming, graph algorithms, local search, ...) into an exact algorithm that provides good performance out of the box and is continuously improving. This tutorial gives an overview of CP Optimizer for planning and scheduling: typical applications, modeling concepts with examples, ingredients of the automatic search, tools and performance.

The complexity of and algorithms for nonuniform CSPs given by restricting the constraint language, that is, the types of allowed constraints, have attracted much attention for more than 40 years since Schaefer's pioneering work classifying the complexity of the Generalized Satisfiability problem. The subsequent study included the discovery of ever growing number of tractable classes and algorithms: max-closed and row-convex constraints, constraints solvable by group-theoretic algorithms, 0/1/all constraints, various constraints admitting a certain algebraic characterizations, several types of digraphs, and many others. On the other hand, a number of hardness results have been obtained, most notably the complexity classification of graph homomorphisms. Feder and Vardi posed the so-called Dichotomy Conjecture that postulates that every nonuniform CSP is either polynomial time solvable or is NP-complete. The majority of research on this kind of CSPs has been revolving around the Dichotomy Conjecture since then. Several approaches have been developed to tackle the Dichotomy Conjecture, through database theory, logic and model theory, and graph theory. The most successful one turned out to be the algebraic approach first developed in a series of works by Jeavons, Cohen and coauthors, and further improved by Bulatov, Jeavons and Krokhin. This approach eventually led to a resolution of the dichotomy Conjecture in 2017. In this tutorial we outline the history of research on nonuniform CSPs and explain the main ideas behind the solution algorithm that solves all nonuniform CSPs that can be solved in polynomial time.