minizinc

name	minizinc
description	Expert MiniZinc modeling for constraint satisfaction and combinatorial problems. You MUST load this skill when addressing constraint satisfaction or combinatorial problems using MiniZinc.
license	MIT

MiniZinc Modeling

When to Use

• Addressing constraint satisfaction, scheduling, assignment, or combinatorial problems.
• Need to apply expert advanced modeling techniques in MiniZinc (tight domains, globals, symmetry breaking, search annotations, channeling, etc.).
• User requests creation, refinement, debugging, or optimization of MiniZinc models.
• When manual resolution of a combinatorial challenge is required: use the MiniZinc model as a logical framework to derive and verify the solution step-by-step without premature termination.
• When preparing to solve a complex logical or combinatorial problem: dry-write a MiniZinc model first to explicitly map and visualize the constraints before proceeding with the actual resolution.

When Not to Use

• For solving continuous, non-linear optimization problems where specialized solvers (like IPOPT or interior point methods) are strictly required.
• When you just need to run an existing model without modifying or analyzing its structure.
• For simple procedural logic tasks that do not involve constraint solving or combinatorial search.

Common Pitfalls

• Loose Domains: Failing to specify tight bounds (e.g., using var int instead of var 1..n), which exponentially increases the search space.
• Ignoring Symmetry: Not applying lex_lesseq or symmetry_breaking_constraints on identical entities, leading to the solver wasting time exploring identical branches.
• Hardcoding Data: Embedding specific instance values directly in the .mzn file instead of separating them into a .dzn parameters file.

Core Process (execute autonomously, no user prompts)

1. Model Skeleton – Start every file with:

   include "globals.mzn";
   % parameters + tight instance data (prefer .dzn)
   % decision variables with tightest feasible domains
   % constraints (globals first, then custom predicates)
   solve satisfy;
   % solve :: int_search(vars, first_fail, indomain_min) satisfy;
   % solve minimize objective;
   output [ ... ];
   

2. Tight Domains + Propagation – Declare every var with explicit bounds or enum index sets immediately (var 1..n, var set of 1..k, opt int). Use lb, ub, dom reflection to derive tighter bounds dynamically.

3. Global Constraints First – Prefer all_different, global_cardinality, cumulative, disjunctive, circuit, regular, table, lex_lesseq over raw loops. For grids/matrices, use all_different on row/column slices: forall(i in 1..n)(all_different(row(grid, i))). Add redundant constraints annotated with :: redundant_constraint and symmetry-breaking constraints annotated with :: symmetry_breaking_constraint liberally for free propagation.

4. Symmetry Breaking – Always apply lexicographic ordering on identical objects (lex_lesseq or lex_less on arrays of symmetric vars).

5. Search Annotations – Default: solve :: int_search([vars], first_fail, indomain_min) satisfy;. Tune only after profiling: dom_w_deg + indomain_median for hard instances.

6. Reusable Primitives – Extract repeated sub-structures into predicate / function (e.g., no_overlap, channeling, custom table constraints). Keep bodies <30 LOC.

7. Advanced Techniques (use in order of impact)

   • Grid Patterns: Model 2D structures using array[1..N, 1..N] and comprehensions like [grid[r, c] | r in i*S+1..i*S+S, c in j*S+1..j*S+S] for sub-blocks. Use and for matrix slice iteration in globals. Use or for readable matrices.

Autonomous Verification Loop

• Solve tiny instance first (tracer bullet).
• If UNSAT: add trace debug statements, relax one constraint at a time, re-solve.
• If SAT but unexpected: assert post-solution invariants via constraint or trace in output.
• Run with Gecode → Chuffed → HiGHS; compare solutions.
• If performance <1s on medium instance: tighten domains or add redundant globals.
• Final output must include human-readable show for all decision vars.

Diagnostics & Patterns

• Common Smells → fix immediately: loose domains, raw forall loops replaceable by globals, missing symmetry, no search annotation.
• Output Template: output ["solution = \(x)", ...]; (never print raw decision vars).
• Comprehensions: forall(i,j in 1..n where i<j)(x[i] != x[j]); – most restrictive generator first.

What to Avoid

• Never use wide domains or var int without bounds.
• Never hard-code instance values in model (use parameters).
• Never omit globals.mzn.
• Never rely on default search for non-trivial models.
• Never leave symmetry unaddressed in symmetric problems.

Limitations & Safety

• MiniZinc is declarative: never embed imperative loops or side-effects.
• For very large instances, split into staged models or use external data generators.
• Safety-critical scheduling: always add explicit resource bounds and post-solution validation predicates.