Skip to content

Expose missing native propagators through MiniZinc and FlatZinc - #253

Draft
zayenz wants to merge 14 commits into
feature/inter-distancefrom
feature/minizinc-registry
Draft

zayenz wants to merge 14 commits into
feature/inter-distancefrom
feature/minizinc-registry

Conversation

@zayenz

@zayenz zayenz commented Oct 10, 2026 •

Copy link
Copy Markdown
Member

Several MiniZinc relations use decompositions even though Gecode has matching propagators. This PR connects them through the standard solver hooks and exposes the remaining Gecode-specific constraints through gecode.mzn overloads and typed FlatZinc declarations.

Standard syntax selects native propagators for count inequalities, conditionals, n-ary integer products, nondeterministic regular constraints, optional scheduling, and extrema. Gecode-specific predicates cover task types, successor paths, singleton set comparisons, reified products, and minimum distance from a distance matrix. Annotations select basic, advanced, or combined algorithms and single or pairwise minimum-distance propagators.

Fixed-base float power and inverse logarithm use explicitly rounded MPFR bounds to preserve exact solutions. The implementation handles base-one powers and shared variables. Divmod result bounds reach FlatZinc before dependent linear constraints are posted. Compiler rounding flags match the parent branch.

Predicate documentation describes the relations, index conventions, empty inputs, and caller-supplied scheduling equalities. The new MiniZinc declarations and predicates use Zincite formatting, with manual corrections for multiline bodies and assertion chains. Gecode set ordering is documented explicitly. General variable-base/variable-exponent float power remains unsupported.

GitHub stack #254: #249 → #247 → #253. This PR is based on #247 (feature/inter-distance).

Validation:

  • Release build of fzn-gecode and gecode-test.
  • 135 FlatZinc and 73 float transcendental regression tests passed with the parent branch’s compiler flags, including exact fixed-base powers and inverse logarithms.
  • Compilation and execution of all 87 typed leaves, 88 facade cases, and 55 standard automatic-route cases.
  • 35 additional exhaustive/routing cases for the native arithmetic, minimum-distance, and NFA APIs in the updated parent.
  • Changelog generation and whitespace checks.
  • MiniZinc documentation generation and verification that the documentation commits change only comments.

The Challenge measurements below preceded restoration of the parent compiler flags and the local MPFR correction. They do not isolate those changes or establish performance of the final float implementation.

MiniZinc Challenge validation (corpus a8448864fc56162583f24aaf9c25653d93f83765, MiniZinc 2.10.1):

  • Compiled 350 of 363 distinct model/include groups against both parent and PR libraries after recorded historical compatibility repairs. The remaining 13 have missing inputs or old source incompatibilities; none fails only on the PR.

  • Tested one structurally small official instance for each of 48 models whose flattened constraints select modified routes, plus five conservative controls, using a five-second search limit. No automatic-route solver errors or invalid final assignments were observed. Some cases reach the time limit without an incumbent.

  • Eight models received three paired follow-up runs with a ten-second search limit and six solver threads. Median completed solve times improved for compression (4.427 to 4.000 s), valve-network (5.703 to 5.178 s), and 2014 liner fm3_11 (4.455 to 4.093 s). 2019 liner fm3_3 increased from 2.645 to 2.917 s, with overlapping ranges. All completed pairs proved the same optimum. These small, parallel samples do not establish a general speedup.

  • Tested six explicit native formulations: nvalues in physician scheduling, steel-mill slabs and peaceable queens; set at-most-one in Steiner systems; set-target count in Unison; joint divmod in rotating workforce. They exposed the divmod bound issue, now fixed; all six original/native workforce follow-up runs returned checked solutions. No clear formulation speedup was established, and steel-mill nvalues produced worse incumbents.

  • The divmod MiniZinc facade also passed exhaustive checking of all 66 signed dividend/divisor tuples in the selected small domains. Final assignments were pinned as equality constraints in fresh compilations of the original models, preserving declared domains and ub/lb semantics.

  • Formatting: all 27 edited MiniZinc files parse with Zincite and preserve comments and code tokens (apart from optional trailing commas). Documentation generation, 55 automatic-route cases, 35 native API cases, and 91 current facade cases passed. The 67 obsolete cases in an earlier scratch suite produce the same compile errors before formatting.

@zayenz
zayenz added this pull request to stack #254 October 10, 2026 18:20

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant