Propagators are central to the success of constraint programming, that is contracting functions removing values proven not to be in any solution of a given constraint. The literature contains numerous propagation algorithms, for many different constraints, and common to all these propagation algorithms is the notion of correctness: only values that appear in no solution to the respective constraint may be removed.

In this paper half-checking propagators are introduced, for which the only requirements are that identified solutions (by the propagators) are actual solutions (to the corresponding constraints), and that the propagators are contracting. In particular, a half-checking propagator may remove solutions resulting in an incomplete solving process, but with the upside that (good) solutions may be found faster. Overall completeness can be obtained by running half-checking propagators as one component in a portfolio solving process. Half-checking propagators opens up a wider variety of techniques to be used when designing propagation algorithms, compared to what is currently available.

A formal model for half-checking propagators is introduced, together with a detailed description of how to support such propagators in a constraint programming system. Three general directions for creating half-checking propagation algorithms are introduced, and used for designing new half-checking propagators for the cost-circuit constraint as examples. The new propagators are implemented in the Gecode system.

Modern board games are a rich source of interesting and new challenges for combinatorial problems. The game Nmbr9 is a solitaire style puzzle game using polyominoes. The rules of the game are simple to explain, but modelling the game effectively using constraint programming is hard. This abstract presents the game, contributes new generalized variants of the game suitable for benchmarking and testing, and describes a model for the presented variants.

The question of the top possible score in the standard game is an open challenge.

Modern board games are a rich source of entertainment for many people, but also contain interesting and challenging structures for game playing research and implementing game playing agents. On the other hand, the complex structures increase the implementation burden, with complex rules and intricate representations needed.

We study the game Patchwork, a two player strategy game using polyomino tile drafting and placement. The core polyomino placement mechanic is implemented in a constraint model using regular constraints, extending and improving the model in Modeling Irregular Shape Placement Problems with Regular Constraints with: explicit rotation handling; optional placements; and new constraints for exact resource usage.

Crucial for implementing good game playing agents is to have great heuristics for guiding the search when faced with large branching factors. Placing tiles is done using a strategy. The strategy is divided into two parts: a policy used for placing parts and an evaluation used to select among different placements. Policies are designed based on classical packing literature as well as common standard constraint programming heuristics. For evaluation, global propapation guided regret is introduced, choosing placements based on not ruling out later placements.

Extensive evaluations are performed, showing the importance of using a good evaluation and that the proposed global propapation guided regret is effective.

Kingdomino is introduced as an interesting game for studying game playing: the game is multiplayer (4 independent players per game); it has a limited game depth (13 moves per player); and it has limited but not insignificant interaction among players.

Several strategies based on locally greedy players, Monte Carlo Evaluation (MCE), and Monte Carlo Tree Search (MCTS) are presented with variants. We examine a variation of UCT called progressive win bias and a playout policy (Player-greedy) focused on selecting good moves for the player. A thorough evaluation is done showing how the strategies perform and how to choose parameters given specific time constraints. The evaluation shows that surprisingly MCE is stronger than MCTS for a game like Kingdomino.

All experiments use a cloud-native design, with a game server in a Docker container, and agents communicating using a REST-style JSON protocol. This enables a multi-language approach to separating the game state, the strategy implementations, and the coordination layer.

Sheet metal cutting using lasers is ubiquitous in the industry, and is used to produce everything from home decorations to excavator scoops. Metal waste is costly for the industry, both in terms of money, but also in terms of an increased environmental footprint. Tomologic develops a unique optimisation system that can reduce this waste drastically. This paper presents a CP approach to the Laser Cutting Path Planning Problem (LCPPP), a very hard important sub problem within the Tomologic optimisation system. A solution to the LCPPP is, given a packing of some details on a metal sheet, an ordering of the cuts necessary to separate the details from the sheet. The problem is complicated by physical factors such as heat from the laser beam, or details moving or flexing. In the paper, we explain the problem in detail and present our CP approach that we developed for solving the problem. The possibility (in CP) of custom search heuristics turned out to be crucial to be able to solve the problem efficiently, as these could be made to guide the search to good first solutions.

Modeling and Programming with Gecode provides comprehensive documentation of how to model and program with Gecode.

The first part of the document explains modeling and solving constraint problems with Gecode. It explains how to program, compile, link, and execute these models. It provides an overview of integer, Boolean, and set variables and constraints, modeling support, search, and Gist. This is complemented by a collection of interesting case studies of how to model with Gecode.

The remaining, more advanced, parts are about programming with Gecode. They explain in great detail and with numerous examples the concepts and techniques for programming constraints, branchings, search engines, and new variable types with Gecode. The parts’ coverage puts users on par with Gecode’s developers.

This paper introduces propagator groups as an abstraction for controlling the execution of propagators as implementations of constraints. Propagator groups enable users of a constraint programming system to program how propagators within a group are executed.

The paper exemplifies propagator groups for controlling both propagation order and propagator interaction. Controlling propagation order is applied to debugging constraint propagation and optimal constraint propagation for Berge-acyclic propagator graphs. Controlling propagator interaction by encapsulating failure and entailment is applied to general reification and constructive disjunction. The paper describes an implementation of propagator groups (based on Gecode) that is applicable to any propagator-centered constraint programming system. Experiments show that groups incur little to no overhead and that the applications of groups are practically usable and efficient.

The regular constraint is a powerful global constraint with many possible uses. It was introduced to model certain common constraints in rostering problems. In this paper we show how to use it to model placement problems with irregular shapes. The technique is illustrated by solving Pentominoes and Solitaire Battleships. The efficiency of the basic model is improved by projecting out irrelevant information. Experimental results on Pentomino packing benchmark instances indicate that this simple approach can be competitive with specialized algorithms. From the applications we can identify some areas for improvement in the implementation of regular constraints.

This thesis explores three new techniques for increasing the efficiency of constraint propagation: support for incremental propagation, improved representation of constraints, and abstractions to simplify propagation.

Support for incremental propagation is added to a propagator-centered propagation system by adding a new intermediate layer of abstraction, advisors, that capture the essential aspects of a variable-centered system. Advisors are used to give propagators a detailed view of the dynamic changes between propagator runs. Advisors enable the implementation of optimal algorithms for important constraints such as extensional constraints and Boolean linear in-equations, which is not possible in a propagator-centered system lacking advisors.

Using Multivalued Decision Diagrams (MDD) as the representation for extensional constraints is shown to be useful for several reasons. Classical operations on MDDs can be used to optimize the representation, and thus speeding up the propagation. In particular, the reduction operation is stronger than the use of DFA minimization for the regular constraint. The use of MDDs is contrasted and compared to a recent proposal where tables are compressed.

Abstractions for constraint programs try to capture small and essential features of a model. These features may be much cheaper to propagate than the unabstracted program. The potential for abstraction is explored using several examples.

These three techniques work on different levels. Support for incremental propagation is essential for the efficient implementation of some constraints, so that the algorithms have the right complexity. On a higher level, the question of representation looks at what a propagator should use for propagation. Finally, the question of abstraction can potentially look at several propagators, to find cases where abstractions might be fruitful.

An essential feature of this thesis is an novel model for general placement constraints that uses regular expressions. The model is very versatile and can be used for several different kinds of placement problems. The model applied to the classic pentominoes puzzle will be used through-out the thesis as an example and for experiments.

While incremental propagation for global constraints is recognized to be important, little research has been devoted to how propagator-centered constraint programming systems should support incremental propagation. This paper introduces advisors as a simple and efficient, yet widely applicable method for supporting incremental propagation in a propagator-centered setting. The paper presents how advisors can be used for achieving different forms of incrementality and evaluates cost and benefit for several global constraints.

In this thesis an operational semantics for a subset of the Java Virtual Machine (JVM) is developed and presented. The subset contains standard operations such as control flow, computation, and memory management. In addition, the subset contains a treatment of parallel threads of execution.

The operational semantics are embedded into a μ-calculus based proof assistant, called the VeriCode Proof Tool (VCPT). VCPT has been developed at the Swedish Institute of Computer Science (SICS), and has powerful features for proving inductive assertions.

Some examples of proving properties of programs using the embedding are presented.