Choco-solver

choco-parsers is an extension for the Choco solver designed to handle models in various formats. It provides specialized parsers for converting low-level and intermediate solver input languages into formats compatible with the Choco ecosystem.

Supported formats include:

• FlatZinc: A low-level solver input language (the target language for MiniZinc).
• XCSP3: An intermediate, integrated XML-based format.
• DIMACS CNF: The standard input file format used in SAT solver competitions.

To use Choco Solver, you must meet the following requirements:

• JDK 8 or higher.
• An Integrated Development Environment (IDE) (e.g., IntelliJ IDEA, Eclipse) is recommended for development.
• For testing without installation, the Choco online IDE is available.

Choco-solver is a Java library for Constraint Programming (CP) used to solve combinatorial search problems. It provides a declarative language to describe problems using variables, domains (possible values), and constraints (predicates).

Core Workflow:

1. Modeling: You define variables (Integer, Boolean, Set, Graph, or Real) and apply constraints (e.g., AllDifferent, Cumulative) to them.
2. Solving: The solver uses a combination of propagation (filtering values that violate constraints) and space reduction (typically via depth-first search) to find solutions.

The library is designed to be a 'black-box' for easy use, but it is also extensible, allowing users to implement new constraints or custom search strategies.

Beyond finding any valid solution, you can define an objective to guide the solver toward an optimal one. In Choco, this typically involves minimizing or maximizing a specific variable or expression.

Example: In a Golomb ruler problem, the objective is to minimize the position of the last mark (tick_m).

In Choco, a constraint is a container composed of one or more propagators. To implement a custom constraint, you must create a Java class that extends Propagator<V>, where V is the type of variable the propagator manages (e.g., IntVar, BoolVar, SetVar, or Variable).

A complete propagator implementation requires:

1. A Constructor that calls super(vars, priority, reactToFineEvt).
2. The propagate(int evtmask) method to implement the filtering algorithm.
3. The isEntailed() method to check if the constraint is satisfied by the current domains.

Note: When a propagator is instantiated, an array of its variables is automatically created and named vars. You must not modify the order of elements in this array.

public class MyPropagator extends Propagator<IntVar> {
    // Implementation details...
}

To create a custom constraint for use in Choco, you must implement a filtering algorithm that updates the domains of the participating variables based on the constraint's logic.

This tutorial uses the implementation of a sum constraint as a reference: $$\sum_{i = 1}^{n} x_i \leq b$$ where $x_i$ are distinct variables and $b$ is a constant.

A basic filtering algorithm for this constraint follows these steps:

1. Compute $F = b - \sum_{i = 1}^{n} \underline{x_i}$ (where $\underline{x_i}$ is the lower bound of variable $x_i$).
2. Update each variable's domain: $\forall i \in [1,n], x_i \leq F + \underline{x_i}$.

Note: If $F < 0$, the constraint is unsatisfiable.

Choco-solver integrates with several community tools and formats:

• File Formats: Parsers for XCSP3 and MiniZinc formats.
• Python Integration: Embedded in PyCSP3, a Python library for modeling and solving combinatorial problems.
• Continuous Solving: Relies on Ibex-lib for real variable/constraint solving.
• Boolean Satisfaction: Integrates a solver based on MiniSat for high-performance logical constraints.

When building complex models, consider these two optimization techniques:

1. Redundant Constraints: Adding constraints that are logically implied by existing ones can reinforce propagation and help the solver detect impossible combinations earlier.
2. Symmetry-Breaking Constraints: Adding constraints that prevent the solver from exploring solutions that are merely permutations or symmetric versions of previously found solutions. This significantly reduces the search space.

Choco provides a comprehensive suite of tools for constraint programming in Java, including:

• Variable Types: Support for integer, boolean, and set variables.
• Constraints: Over 70 state-of-the-art constraint implementations.
• Search Framework: The PLM framework enables configurable searches and widely-used search strategies.
• Problem Types: Handles both satisfaction and optimization (mono and multi-objective) problems.
• Execution: Supports multi-threaded resolution.
• Parsing: Includes parsers for MiniZinc and XCSP3 instances.
• Advanced Features: Supports explanations, graph variables/constraints, and gentle binding to Ibex for real variables and constraints.

The regular constraint is used to construct valid fixed-sized words based on a specific vocabulary and grammar (defined by a DFA). It is particularly useful for enforcing patterns in solutions, such as scheduling constraints (e.g., "a nurse cannot work a late night shift followed by a day shift").

To apply it, you pass a collection of decision variables (e.g., a BoolVar[] or a column from a BoolVar[][] matrix) and an IAutomaton object to model.regular(variables, automaton).post().

Global constraints capture common patterns and use efficient propagation algorithms to prune the search space. A common example is allDifferent, which ensures that all variables in a given set take distinct values.

You can post multiple constraints at once using model.post(...).

To create auxiliary variables for diagonal constraints in an 8-queens problem, you can map existing variables through arithmetic expressions using .intVar():

IntVar[] diag1 = IntStream.range(0, n)
                          .mapToObj(i -> vars[i].sub(i).intVar())
                          .toArray(IntVar[]::new);

model.post(
    model.allDifferent(vars),
    model.allDifferent(diag1)
);