ABSTRACT. Solver-independent modelling languages such as MiniZinc are widely used because they enable rapid prototyping of complex optimisation models without committing to a particular solver technology. However, when using a fixed constraint programming solver, one can extend it with custom problem-specific propagators. This can potentially achieve significantly stronger propagation and improved performance. In contrast, within a solver-independent framework, such constraints are typically expressed through decompositions into simpler primitives, which may weaken propagation and increase runtime. This paper presents an extension to MiniZinc that enables specifying custom propagators directly at the modelling level. These propagators are executed via solver callbacks, preserving solver independence while enabling specialised propagation. Beyond modelling-level propagators, our framework enables the integration of externally implemented propagators, making it possible to incorporate propagation for complex black-box functions, such as simulation models. We demonstrate that this enables the rapid development of efficient problem-specific propagators and facilitates hybrid white-box/black-box optimisation approaches.

ABSTRACT. The minimum-distance constraint min_distance(D, x, z) links selected-point variables x with a variable z denoting the smallest distance between any selected pair. A direct CP encoding introduces one auxiliary distance variable per pair and then constrains the objective to be the minimum of those variables. This encoding is clear and portable, but it also creates a quadratic family of variables and propagators. It can also spend memory representing holes in auxiliary distance domains, even when branch-and-bound only needs useful (lower) bounds on the minimum distance. This paper studies propagation algorithms for the minimum-distance constraint in Gecode. The implemented variants include pairwise propagators, a global support scan, advisor-backed support maintenance, and a matching-based upper-bound propagator. A motivating example for studying these algorithms is p-dispersion with distance constraints, where the minimum-distance constraint is central and pair-specific lower-bound thresholds are part of the model. Preliminary benchmarks on p-dispersion instances from the literature indicate that direct propagation of this constraint can reduce decomposition overhead, but the experiments should be read as an implementation study rather than a complete p-dispersion solver comparison. The organisation of the propagator is important: full global scans can be too expensive, advisor-backed incremental state maintenance and matching-based bounds help on the indexed model, and pairwise bounds remain a strong baseline.

ABSTRACT. Interactive Constraint Acquisition (CA) can assist in modeling constraint problems by acquiring constraints through a query-based interaction with the user. However, existing methods often require a large number of queries. We aim to address this limitation by introducing constraint-specification-based generalization queries, which lift individual learned constraints to higher-level specifications that capture entire sets of constraints at once. We then propose \gqgen, a machine learning-based method to extract such specifications from the learned and excluded constraints during the acquisition process and show how it can be integrated directly within any existing interactive CA algorithm. Our experiments show that our proposed approach reduces the number of queries substantially (by up to 95%), while our user study demonstrates that LLM-based natural language formulations of our generalization queries are understandable to users.

ABSTRACT. Paramita is a Python framework that provides a unified, plugin-based interface for interacting with external tools from the Satisfaibility domain (e.g. SAT and MaxSAT solvers). These tools can be implemented in C++ or Python. The framework follows a strict separation between interface definitions and concrete implementations. Solvers and encoders in C++ are compiled as shared libraries and loaded at runtime. Solvers implementing IPASIR, IPASIR-UP and IPAMIR C++ interfaces can be directly integrated in Paramita with almost no effort. Paramita also supports a higher level modelling language for Non-CNF formulas, extendend with PB constraints and linear objective functions. Paramita is suitable for a wide range of combinatorial optimization and satisfiability tasks. This paper describes the architecture, solver and interfaces provided by the framework, the modelling language and other features.

ABSTRACT. Logic puzzles like Sudoku have been very popular for several decades, some videos showing the solution steps for a complex Sudoku variant instance have over 10 million views. This makes this problem domain an ideal area to demonstrate the advantages of using Constraint Programming to a wider audience. We present an interactive application for solving Sudoku variants, extending the classical Sudoku grid with a variety of additional constraints. The aim is not just to search for solutions of a given puzzle, but to help a user to find a solution interactively. We use an off-the-shelf constraint solver, Choco-solver, to model and propagate 200 common Sudoku variant constraints. This uses a combination of specific global constraints and table constraints to describe feasible or infeasible tuples. In other cases, we use logical expressions over basic constraints to model complex side constraints. The user can add constraints interactively if the solver does not find the solution by propagation alone, or rely on an agent to add deduced constraints dynamically. We evaluate the solver on different data sets, and show that over 97% of the problems in the 2025 Sudoku Grand Prix can be solved by the tool, and that many popular, complex puzzle instances can be solved by a handful of manual constraints and propagation alone.

ABSTRACT. Helmut Simonis's 2005 ModRef paper, Sudoku as a Constraint Problem, used standard 9x9 Sudoku as a compact constraint-programming laboratory for comparing propagation-oriented models. This paper extends that setup to Sudoku puzzles of sizes 6x6, 9x9, 16x16, 25x25, and 36x36. We generate 32,000 unique-solution base puzzles and run 170,000 hardness walks that add clues back to the puzzles, generating 402,201 additional, simpler instances. These walks ensure that every studied size includes instances in easier hardness buckets. The original hardness categories identified by Simonis remain useful, but the grid size changes the observed propagation behaviour. No initially generated 25x25 or 36x36 puzzle is solved without search, even with domain-consistent propagation and domain shaving. Puzzle generation uses Gecode and OR-Tools, and hardness testing uses Gecode.

ABSTRACT. Reductions and gadgets are key tools in computational complexity, with gadgets serving as the building blocks of reductions. Despite their importance, gadget construction has traditionally been ad hoc. We present a method to compute gadgets automatically, enabling systematic reductions and offering insights for both theory and practical solver design.

ABSTRACT. Access to high-quality benchmark instances is essential for developing new algorithms and constraint models, as well as for comparing existing approaches. However, hand-crafted instances are often time-consuming to produce and may offer limited coverage of the relevant instance space. Consequently, automated benchmark instance generation has been widely studied across optimisation and related fields. In this work, we study AutoIG, a previously proposed constraint-based automated instance generation framework that combines automated algorithm configuration, constraint modelling, and constraint solving to generate instances of a specified difficulty for a target solver. A key limitation of AutoIG is that it does not explicitly encourage diversity among the generated instances. This can lead to benchmark sets that satisfy the desired difficulty requirements but provide limited variation in solver behaviour. As a preliminary step towards addressing this limitation, we investigate three simple mechanisms for promoting diversity in the performance space. That is, we aim to generate instances that not only meet a target difficulty level, but also induce diverse performance from the target solver. Experiments on two problem classes and two solvers show promising potential, while also revealing several open challenges, including how diversity should be defined and measured, and how diversity-promoting mechanisms affect the search process during instance generation.

ABSTRACT. In higher education, activity-based teaching has become increasingly popular as an alternative or complement to lecture-based teaching. The topic-swapping peer-teaching classroom activity is as follows: first, each student acquires a topic; then, over rounds, they form pairs to swap their acquired topics within the pair until each topic has been acquired once by each student. The idea behind the topic swapping activity is for students to: (1) acquire knowledge about each topic and (2) interact with many students. The topic-swapping activity can be formulated as a constrained optimisation problem (COP). An optimal solution to the COP is where (1) each formed student pair is unique and (2) each student acquires a novel topic each round (one they have not had previously). We have modelled the topic-swapping activity COP in the MiniZinc modelling language. From our findings, constraints (1) and (2) often conflict, resulting in no such optimal solution. Additionally, our experiments show that finding solutions even for small instances is difficult.

ABSTRACT. At a wedding, a seating plan can satisfy capacity limits, grouping requests, separation requests, and balance constraints while still leaving a guest at a table with little shared ground for conversation. This paper introduces Table Talk Tuning (TTT), a small constraint modelling problem drawn from a real wedding-seating case. The name points to the part of the task that ordinary seating constraints leave implicit: giving each guest at least one plausible conversation topic shared with enough tablemates. TTT uses guest topic scores to prefer tables where each guest has a strongest shared topic that enough tablemates can sustain together. The conversation score is optimised after structural terms for table slack and gender balance, so social fit becomes part of the seating objective rather than a post-processing check. We present a MiniZinc model, three synthetic instance families from 10 to 150 guests, a reproducible benchmark pipeline, and a native Gecode implementation for studying objective-aware search. The experiments compare MiniZinc solvers and native search strategies. They show that the conversation terms change the returned seatings on matched instances, and that objective handling matters in practice even when the underlying model is fixed.

ABSTRACT. Planning domains are usually represented in first-order logic. However, historically, most of the planners have been using grounded problem representations. Since grounding can lead to a combinatorial explosion, and thus make some problems intractable, the community has developed techniques to deal with hard-to-ground problems. Those techniques include, for example, splitting action schemas, or partially grounding actions to relevant instantiations for the goal at hand. Recently, a new family of planners which work directly on lifted representations has emerged. However, most of these so-called lifted planners still rely on grounding to some extent. With the aim of broadening the range of approaches to lifted planning, in this work we present a satisfiability-based lifted planner that works on first-order representations and does not rely on grounding at all. We encode the lifted planning task into a quantifier-free formula with uninterpreted functions, in first-order logic with equality. Despite showing higher solving times than the state-of-the art, the planner proves to consume very little memory and is competitive on hard-to-ground instances.

ABSTRACT. Auto-grading student constraint models requires a checker to validate candidate solutions against the problem specification. In practice, for example in the Coursera MOOC on MiniZinc, the checker is developed separately from the teacher's own constraint model. This duplicates effort and risks inconsistencies that produce confusing feedback and unfair grades. We present a framework for CPMpy in which the checker is automatically derived from the teacher's constraint model. By adding a feedback template to each constraint, granular feedback is returned when a student solution violates a specified constraint, domain, or objective. Decision variables in the teacher's model that are intentionally hidden from the student are assigned consistently via a Maximal Satisfiable Subset computation. The same model also provides a performance baseline for grading, generates instances of various difficulty, and can be obfuscated and distributed for local checking. We illustrate the approach on an example Flexible Jobshop Scheduling project, demonstrating violation detection on a toy instance, and checker performance on larger instances.