From 9063b4ec29fce58a7ff51ca60cbe9704de49dd49 Mon Sep 17 00:00:00 2001 From: Pavel Konov Date: Mon, 7 Sep 2026 14:05:05 -0700 Subject: [PATCH] Expose native optimization strategies through MiniZinc --- .github/pr/minizinc-native-controls.md | 59 +++++ CMakeLists.txt | 4 + docs/solver-parity/FLATZINC-COMPILER.md | 5 + docs/solver-parity/FLATZINC-DRIVER.md | 8 + docs/solver-parity/MINIZINC-CONTROLS-QA.md | 116 +++++++++ docs/solver-parity/MINIZINC.md | 117 ++++++++- docs/solver-parity/NATIVE.md | 11 +- docs/solver-parity/README.md | 4 +- doxygen/optimize.hh | 16 +- gecode/optimize/flatzinc.cpp | 6 +- gecode/optimize/native.cpp | 80 ++++--- gecode/optimize/native.hpp | 37 ++- gecode/optimize/native_preprocess.hpp | 3 + gecode/optimize/native_presolve.cpp | 126 ++++++++++ test/optimize/flatzinc.cpp | 14 ++ test/optimize/flatzinc_driver.cpp | 97 +++++++- test/optimize/flatzinc_driver_cli.py | 80 ++++++- .../minizinc-fixtures/mzn-native-controls.mzn | 11 + .../minizinc-fixtures/mzn-native-knapsack.mzn | 9 + test/optimize/minizinc_configure.py | 6 + test/optimize/minizinc_registration.py | 177 +++++++++++++- test/optimize/native_auto.cpp | 87 ++++++- test/optimize/native_presolve.cpp | 92 ++++++- test/optimize/native_race.cpp | 27 ++- tools/flatzinc/fzn-gecode-optimize.cpp | 225 +++++++++++++++++- tools/flatzinc/gecode-optimize.msc.in | 24 +- 26 files changed, 1378 insertions(+), 63 deletions(-) create mode 100644 .github/pr/minizinc-native-controls.md create mode 100644 docs/solver-parity/MINIZINC-CONTROLS-QA.md create mode 100644 test/optimize/minizinc-fixtures/mzn-native-controls.mzn create mode 100644 test/optimize/minizinc-fixtures/mzn-native-knapsack.mzn diff --git a/.github/pr/minizinc-native-controls.md b/.github/pr/minizinc-native-controls.md new file mode 100644 index 0000000000..0ce950aca8 --- /dev/null +++ b/.github/pr/minizinc-native-controls.md @@ -0,0 +1,59 @@ +# Expose native optimization strategies through MiniZinc + +MiniZinc users can now select automatic, racing, ordinary or explicitly +configured native solving through the experimental Gecode Optimize registration. +The default remains structural automatic selection. Solver flags expose the +existing improvements without requiring C++ integration or search annotations. + +MiniZinc often emits binary decisions as integer `0..1` variables and wraps a +linear objective in an auxiliary variable. Preserve the source types and checks +while recognizing those binary domains internally. Bounded automatic presolve +eliminates one safely defined affine objective auxiliary, preserves any +restrictive auxiliary bounds, and reconstructs/checks its original value. This +lets ordinary MiniZinc knapsack models reach the existing exact DP route. + +## Changes + +- Advertise 21 namespaced MiniZinc controls for automatic feature switches, + racing allowances, checked LP frequency/tightening, root covers, search order, + reliability probes, Hamming neighborhoods, resource caps and diagnostics. +- Add `NativeAutoSettings` / `solve_native_auto_configured` and race + automatic-candidate settings. Disabled mechanisms remain disabled in reduced + and independent component solves. Explicit settings reject incompatible modes + or missing dependencies before solving. +- Dispatch every strategy with the remaining frontend time and shared solver + node budget. Optional diagnostics distinguish requested settings from actual + policy, LP/cut/probe activity, and neighborhood completion or skip reasons. +- Document supported combinations, executable examples and racing overhead. + Sequential exploration/restarting can increase CPU work or solve time; + several seconds or longer may find a much better strategy for a long solve. +- Track registration inputs in CMake so rebuilds update installed flags as well + as build-tree flags; verify the installed relative registration in place. + +The experimental native integer scope is unchanged. This does not add numerical +LP/MILP/QP MiniZinc model support, conflict learning or parallel racing. The +benchmark dashboard is outside this PR. + +## Validation + +All **75 CTest entries pass**, as do **135 real MiniZinc checks** against each of +the build registration, installed registration and a checked-LP-disabled harness. +Three backend-free native coordinator tests also pass. + +See [the QA walkthrough](../../docs/solver-parity/MINIZINC-CONTROLS-QA.md) for +the actual MiniZinc 2.10.1 commands, independent objective/witness checks, +algorithm activity and regression results. Tests also cover strict flag +forwarding, zero/finite budgets, output/proof markers, original domain and +objective reconstruction, and unavailable checked LP. + +## Review base + +This is a separate incremental PR: `codex/minizinc-native-controls` targets +`codex/solver-parity-pr` (`884795c874174fd293bab554ee8a544fe45580c1`). That +prerequisite branch contains the earlier optimization contribution. Its tree +matches integration checkpoint `b11a57c1d`; the new branch is based directly on +the review commit so the comparison contains only this MiniZinc work. + +The repository's configured remote is a local checkout. Publish the prerequisite +review branch and this branch to the chosen GitHub fork before opening the +stacked pull request. No remote PR or merge is implied by this local preparation. diff --git a/CMakeLists.txt b/CMakeLists.txt index d1cae016b1..b83e676312 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1431,6 +1431,10 @@ if(GECODE_OPTIMIZE_MINIZINC_REGISTRATION) endif() set(_gecode_optimize_msc_template "${PROJECT_SOURCE_DIR}/tools/flatzinc/gecode-optimize.msc.in") set(_gecode_optimize_msc_encoder "${PROJECT_SOURCE_DIR}/tools/flatzinc/configure-optimize-msc.cmake") + # execute_process below generates the install registration at configure time. + # Keep it in sync when solver flags or JSON encoding change between builds. + set_property(DIRECTORY APPEND PROPERTY CMAKE_CONFIGURE_DEPENDS + "${_gecode_optimize_msc_template}" "${_gecode_optimize_msc_encoder}") set(_gecode_optimize_build_msc "${PROJECT_BINARY_DIR}/minizinc/$/gecode-optimize.msc") # Target paths are expanded before the encoder escapes them as JSON. This # also supports multi-configuration builds and source/build paths with quotes. diff --git a/docs/solver-parity/FLATZINC-COMPILER.md b/docs/solver-parity/FLATZINC-COMPILER.md index 7bb6713ea6..a189d13668 100644 --- a/docs/solver-parity/FLATZINC-COMPILER.md +++ b/docs/solver-parity/FLATZINC-COMPILER.md @@ -34,6 +34,11 @@ lost through an incomplete registry observer. Each source namespace/index maps to a stable model variable; repeated declaration aliases retain separate source mapping entries and output positions. Bool and int slot zero are different. +An integer domain contained in `0..1` uses an equivalent internal Binary variable +so native binary algorithms can recognize MiniZinc's integer decision encoding. +This is based only on original declarations, assignments and domain restrictions; +source type, aliases, integer output and all original domain checks are retained. + An immutable owning artifact is published only after every source predicate, objective, control annotation and output entry is admitted. Unknown predicates, equality reification, other globals, float/set variables and unhandled diff --git a/docs/solver-parity/FLATZINC-DRIVER.md b/docs/solver-parity/FLATZINC-DRIVER.md index 31142c3a93..c19af43473 100644 --- a/docs/solver-parity/FLATZINC-DRIVER.md +++ b/docs/solver-parity/FLATZINC-DRIVER.md @@ -18,6 +18,14 @@ in a FlatZinc comment. Exact feasible-point checking does not certify a numerica optimal bound or infeasibility claim. An unavailable selected backend fails explicitly. There is no automatic backend or legacy-parser fallback. +The native route defaults to structural automatic selection. Namespaced +`--native-*` controls expose automatic feature switches, opt-in racing and +configured LP/search/branching/neighborhood settings; see the complete +[MiniZinc control reference](MINIZINC.md#native-algorithm-controls). The same +flags work in this filename-first direct interface. `--native-diagnostics on` +adds sanitized comment lines describing requested controls and actual work. +Native controls cannot be mixed with `--backend highs`. + See [the compiler](FLATZINC-COMPILER.md) for the admitted signatures and [the capture layer](FLATZINC-CAPTURE.md) for grammar and lifecycle boundaries. Unknown predicates, search annotations, unsupported domains and output types diff --git a/docs/solver-parity/MINIZINC-CONTROLS-QA.md b/docs/solver-parity/MINIZINC-CONTROLS-QA.md new file mode 100644 index 0000000000..6e7995bb8a --- /dev/null +++ b/docs/solver-parity/MINIZINC-CONTROLS-QA.md @@ -0,0 +1,116 @@ +# MiniZinc native controls: QA walkthrough + +Verified locally on macOS ARM64 with pinned MiniZinc **2.10.1**, its matching +standard library, and an isolated Release build. This is correctness, dispatch, +resource and packaging QA; no new performance benchmark or speedup claim is made. + +## Results + +- Full Release regression: **75/75 CTest entries pass**, including FAST, source + truth tables, frontend fault injection, native algorithms and Python bindings. +- Actual MiniZinc build registration: **135 process checks pass**, including + 26 successful native-control scenarios and independent six-decision oracles. +- Installed registration: **135 checks pass** against the actual installed + executable and library using relative `.msc` paths. The executable resolves + libraries through `@loader_path/../lib`, without the build directory. +- Checked-LP-disabled harness: **135 MiniZinc checks plus three native tests + pass**. Runtime inspection confirms the isolated optimization library loads. + Explicit LP requests fail clearly; automatic/native/racing routes still work. + This harness disables native checked LP while retaining other HiGHS APIs. +- Backend-free build: **3/3** automatic, racing and presolve tests pass, including + backend-independent objective-reconstruction and malformed-result checks. +- JSON registration encoder: **10 cases pass**, preserving all 21 controls, + escaped paths and relocatable install paths. + +All optimization witnesses below are checked against independent exhaustive +source-model oracles, including tied optima. The two small six-decision fixtures +both have optimum **12**. The tests check actual work rather than only acceptance +of command-line options. + +| Walkthrough | Observed activity | +|---|---| +| Integer `0..1` knapsack, default auto | Objective auxiliary restored; eligible exact knapsack DP selected. | +| Same model, automatic knapsack disabled | Same optimum; DP route absent. | +| Racing with four nodes per probe | Two probes and selection of automatic route; one shared cumulative node budget. | +| Zero exploration / retained all-different global | Explicit race skip, correct result. | +| Configured reliability | 24 actual probe status calls. | +| Configured Hamming, radius 1 | One attempt and three local status calls; completion reason reported. | +| Configured root LP plus covers | Five LP calls, five checked bounds, four verified cover cuts. | +| Configured updated LP, cuts, reliability, Hamming | 31 checked bounds, four cuts and 20 branching probes. | + +These are small-fixture activity counts, not recommended tuning constants or +general performance predictions. Hamming distance counts flattened binary slots; +the Boolean fixture also contains integer aliases, so one logical Boolean change +can require radius two. Optional mechanisms may correctly skip or do no useful +work on other models. + +The gate verifies flag discovery and forwarding through the real MiniZinc parser, +all four modes, individual/all automatic switches, explicit dependencies, +zero optional allowances, global node limits of zero and one, zero frontier +storage, malformed/overflowing/repeated controls and whole-frontend timeouts. +Every printed completion marker must match the independently computed optimum; +interruptions may print only a checked witness or UNKNOWN. Diagnostic control +characters are sanitized before writing protocol comments. + +The compiler tests verify that internal binary recognition preserves integer +source typing, output, aliases and domains. Native tests cover both signs of the +objective-defining equality, minimization/maximization, objective offsets, +restrictive auxiliary domains, disabled presolve/DP, original model identity and +active mask, supplied starts, shared budgets, cancellation and invalid child +results. No declaration name or `defines_var` annotation is trusted as proof of +equivalence. + +Packaging QA caught a stale configure-time install registration in an existing +build. CMake now tracks the registration template and encoder as configure +dependencies, so changing advertised controls updates both build and install +registrations. The installed artifact contains all 21 controls and passes the +same real-compiler gate in place. + +## Reproduce + +From the solver repository, using the configured build described in +[the MiniZinc setup guide](MINIZINC.md#build-and-installation): + +```sh +cmake --build build/native-structure/native-build -j 4 +ctest --test-dir build/native-structure/native-build --output-on-failure +python3 -B test/optimize/minizinc_registration.py \ + --minizinc ../deps/MiniZinc-2.10.1-aarch64-apple-darwin/bin/minizinc \ + --binary build/native-structure/native-build/bin/fzn-gecode-optimize \ + --registration build/native-structure/native-build/minizinc/Release/gecode-optimize.msc +``` + +To inspect the actual algorithm choices interactively: + +```sh +mzn=../deps/MiniZinc-2.10.1-aarch64-apple-darwin/bin/minizinc +solver="$PWD/build/native-structure/native-build/minizinc/Release/gecode-optimize.msc" +"$mzn" --solver "$solver" --native-diagnostics on \ + test/optimize/minizinc-fixtures/mzn-native-knapsack.mzn +"$mzn" --solver "$solver" --native-mode race \ + --native-race-seconds 0.05 --native-race-nodes 4 --native-diagnostics on \ + test/optimize/minizinc-fixtures/mzn-native-controls.mzn +"$mzn" --solver "$solver" --native-mode configured --native-lp root \ + --native-root-cuts on --native-diagnostics on \ + test/optimize/minizinc-fixtures/mzn-native-controls.mzn +``` + +Select `org.gecode.optimize.experimental` explicitly; the stock Gecode solver +registration does not expose these flags. Racing can increase CPU work or solve +time through exploration and restarting, even when a later strategy is faster. + +The local JSON reports retain process checks, source/compiler/driver/configuration +and MiniZinc library hashes, requested settings, actual policy and work counters: + +- `build/native-structure/native-build/minizinc-controls-registration.json` +- `build/native-structure/native-build/minizinc-controls-installed-registration.json` +- `build/native-structure/native-build/minizinc-controls-ctest.log` +- `build/minizinc-controls-no-lp/summary.json` and `reproduce.py` +- `build/optimize-core/minizinc-controls-ctest.log` + +Build-tree driver SHA256: +`3efb21d82322aff323bd05add9ef9b5b34898a5478d8766df06fb8fd13538669`. +The compiler SHA256 is +`a8489069d77793862102ca5bab5b2e24822d4445226e4262b8d35287a9af702f`. +Other machines need not produce identical binaries or work counts. Remote CI, +Windows runtime behavior and a new sanitizer run are not claimed here. diff --git a/docs/solver-parity/MINIZINC.md b/docs/solver-parity/MINIZINC.md index 6e85f44cc6..a79399da64 100644 --- a/docs/solver-parity/MINIZINC.md +++ b/docs/solver-parity/MINIZINC.md @@ -30,14 +30,117 @@ minizinc --solver /path/to/gecode-optimize.msc model.mzn data.dzn minizinc --solver /path/to/gecode-optimize.msc --solver-time-limit 1000 model.mzn ``` +## Native algorithm controls + +The experimental registration now exposes native algorithm controls through +MiniZinc's solver `extraFlags`. No model annotations are needed. The default +`--native-mode auto` uses bounded structural selection, exact preprocessing and +eligible knapsack DP; it does not run a race unless requested. + +```sh +# Default automatic selection, with an explanation of the actual route. +minizinc --solver /path/to/gecode-optimize.msc \ + --native-diagnostics on model.mzn + +# Compare automatic selection with ordinary search within one solve budget. +minizinc --solver /path/to/gecode-optimize.msc \ + --native-mode race --native-race-seconds 8 --native-race-nodes 50000 \ + --solver-time-limit 120000 --native-diagnostics on model.mzn + +# Explicit checked LP, cuts, reliability branching and a bounded neighborhood. +minizinc --solver /path/to/gecode-optimize.msc \ + --native-mode configured --native-search dfs --native-lp updated \ + --native-root-cuts on --native-branching reliability \ + --native-neighborhood hamming --native-diagnostics on model.mzn +``` + +| Mode | Behavior | +|---|---| +| `auto` (default) | Conservative structural selection; enabled mechanisms still require eligible model structure. | +| `race` | Up to two bounded sequential probes, automatic versus ordinary BAB; restart the selected route if unresolved. | +| `plain` | Direct native BAB, including its existing eligible exact knapsack DP. | +| `configured` | Explicit LP/frontier/branching/neighborhood settings; default is DFS without LP, reliability or neighborhoods. Automatic transformations are omitted. | + +**Racing may increase total CPU work or solve time.** Exploration and restarting +repeat work, and early progress can favor a strategy that eventually loses. +Several seconds or longer may nevertheless identify a much more effective route +for a long solve. Probes run sequentially, with one worker. The nominal exploration +allowance is capped at 25% of the remaining finite solve time; all probes and the +restart share the global deadline and cumulative node allowance. Zero exploration +skips the race and runs the automatic policy. Globals/indicators also skip racing. +This is a heuristic, not a performance guarantee. + +All controls take an explicit value. The following table gives defaults when +omitted; MiniZinc does not forward the advertised defaults as explicit arguments. + +| Flag | Values / default | Scope | +|---|---|---| +| `--native-mode` | `auto`, `race`, `plain`, `configured`; `auto` | All native solves | +| `--native-diagnostics` | `on`, `off`; `off` | All native solves | +| `--native-node-limit` | Unsigned count; unlimited | All native solves; zero permits no search node admissions | +| `--native-auto-presolve` | `on`, `off`; `on` | `auto` / automatic candidate in `race` | +| `--native-auto-components` | `on`, `off`; `on` | `auto` / automatic candidate in `race` | +| `--native-auto-symmetry` | `on`, `off`; `on` | `auto` / automatic candidate in `race` | +| `--native-auto-knapsack` | `on`, `off`; `on` | `auto` / automatic candidate in `race` | +| `--native-race-seconds` | Finite nonnegative seconds; `2` | `race` | +| `--native-race-nodes` | Positive count per probe; `4096` | `race` | +| `--native-search` | `bab`, `dfs`, `best-bound`; `dfs` | `configured` | +| `--native-lp` | `off`, `root`, `updated`; `off` | `configured`; requires checked LP capability when enabled | +| `--native-root-cuts` | `on`, `off`; `off` | `configured` with LP | +| `--native-bound-tightening` | `on`, `off`; `on` | `configured` with LP | +| `--native-lp-interval` | Positive observed bound-change count; `1` | `configured` with updated LP | +| `--native-branching` | `default`, `reliability`; `default` | `configured` frontier search | +| `--native-branching-probes` | Nonnegative status-call count; `128` | Reliability branching | +| `--native-max-open-nodes` | Nonnegative stored-space count; `100000` | `configured` frontier search; not a byte limit | +| `--native-neighborhood` | `off`, `hamming`; `off` | `configured` frontier search | +| `--native-neighborhood-radius` | Nonnegative binary Hamming distance; `1` | Hamming neighborhood | +| `--native-neighborhood-nodes` | Nonnegative local status-call count; `128` | Hamming neighborhood | +| `--native-neighborhood-seconds` | Finite nonnegative local seconds; `0.05` | Hamming neighborhood | + +Automatic switches permit a mechanism; they do not force it onto unsuitable +models. A disabled switch skips that mechanism throughout automatic reduced and +component solves. In racing, `--native-auto-*` affects the automatic candidate; +the ordinary comparator keeps its existing behavior, including eligible DP. +Configured reliability considers eligible binary variables. Hamming search makes +at most one bounded attempt after an incumbent and may skip if there is no +incumbent, no eligible binary decision, or proof finishes first. Hamming distance +counts flattened binary slots: a Boolean and its `bool2int` integer alias count +separately. Such an aliased decision can require radius `2` to change its value. +LP deductions +and cover cuts retain their checked integer contracts. Explicit LP without its +required HiGHS/checked arithmetic support is an error, not a silent fallback. + +Diagnostics are FlatZinc `%` comments reporting the requested mode/settings, +actual backend/policy and available work counters. A request is not evidence that +optional work ran; counters and skip explanations make that distinction visible. +Diagnostics do not enable enumeration or intermediate solutions. The default +solution protocol remains unchanged. Conflicting, irrelevant, duplicated, +malformed and overflowing options are rejected before solving, including +configured-only settings in automatic mode and frontier-only settings with BAB. + +Integer source domains contained in `0..1` are represented as binary decisions +internally while retaining integer output and original domain checks. The +automatic presolve path can remove a narrowly eligible linear objective auxiliary +introduced by MiniZinc, restore its value, and check the original model before +publishing a result. Its domain restrictions are preserved. More complicated +flattened models may still choose ordinary native search; diagnostics explain +the selected route. + +This change exposes **native integer solver controls**. It does not add numerical +LP/MILP or quadratic MiniZinc model support, multiobjective/session/repair/pool +workflows, conflict learning, parallel racing or general search annotations. +Those broader APIs remain separate from this experimental registration. + +## Build and installation + Enable `GECODE_OPTIMIZE_MINIZINC_REGISTRATION=ON` in a top-level build with the optimization FlatZinc driver and native backend enabled. The option defaults to OFF. Optionally set `GECODE_OPTIMIZE_MINIZINC_EXECUTABLE` to an existing pinned compiler to enable the real compiler CTest; configuration never downloads one. ```sh -cmake -S . -B build/native-compat \\ - -DGECODE_OPTIMIZE_MINIZINC_REGISTRATION=ON \\ +cmake -S . -B build/native-compat \ + -DGECODE_OPTIMIZE_MINIZINC_REGISTRATION=ON \ -DGECODE_OPTIMIZE_MINIZINC_EXECUTABLE=/path/to/minizinc cmake --build build/native-compat --target gecode-optimize-minizinc-config ctest --test-dir build/native-compat --output-on-failure -R '^optimize-minizinc-' @@ -86,13 +189,14 @@ process. Neither the driver nor the registration writes `Preferences.json` or The explicit mode accepts: ```text -fzn-gecode-optimize --minizinc [-t MILLISECONDS] MODEL.fzn|- +fzn-gecode-optimize --minizinc [-t MILLISECONDS] [--native-mode MODE ...] MODEL.fzn|- ``` `-t` can precede or follow the filename. `--` ends option parsing, allowing a filename beginning with a hyphen. Exactly one filename and at most one `-t` are -required; unsupported flags, missing values, fractions, negative values, duplicate -options, and unsigned-count overflow are errors. This mode always uses Native +required; unsupported flags, missing values, fractional/negative counts, duplicate +options, and unsigned-count overflow are errors. Native time settings allow +finite nonnegative fractional seconds. This mode always uses Native with the exact guarantee and zero requested gaps. No backend override is accepted. `-t` is an unsigned decimal count of milliseconds. Zero means unlimited, matching @@ -112,6 +216,9 @@ child exit as `ERROR`, including when the child printed `UNKNOWN`. The direct driver interface remains separate: `MODEL.fzn --time-limit SECONDS` retains its existing filename-first syntax, immediate zero deadline, optional explicit HiGHS route, and exit **1** for an ordinary incomplete solve. +It also accepts the native controls above; supplying them with `--backend highs` +is an error. `--node-limit` and `--native-node-limit` are aliases and cannot both +be supplied. The `.msc` does not advertise enumeration, intermediate incumbents, parallel search, randomness, or solver statistics. The driver rejects such flags if diff --git a/docs/solver-parity/NATIVE.md b/docs/solver-parity/NATIVE.md index 9522f430fa..3fd7fcd969 100644 --- a/docs/solver-parity/NATIVE.md +++ b/docs/solver-parity/NATIVE.md @@ -73,7 +73,8 @@ policy implies broad gains on unseen models. ## Optional automatic strategy racing `solve_native_race` is an opt-in C++ entry point for native Gecode, accepting a -`Model` or `ModelSnapshot`. It is not yet surfaced as a MiniZinc/FlatZinc option. +`Model` or `ModelSnapshot`. The experimental [MiniZinc/FlatZinc frontend](MINIZINC.md) +also exposes it with `--native-mode race` and explicit exploration controls. It integrates the automatic presolve, independent components, identical-column symmetry, compact knapsack DP and suitable checked-LP/branching choices above. It compares that automatic route against ordinary native BAB (which also keeps @@ -135,6 +136,14 @@ correctness/resource checks, not a new performance comparison. ## Exact automatic preprocessing +`NativeAutoOptions` combines `SolveOptions` with `NativeAutoSettings`. Call +`solve_native_auto_configured(model, options)` to independently disable presolve, +components, symmetry or knapsack DP. All four settings default to true and permit +eligible work rather than forcing it. The existing `solve_native_auto` overloads +retain their defaults. `NativeRaceOptions::automatic` applies these switches to +the automatic candidate; its ordinary comparator retains eligible knapsack DP. +MiniZinc exposes the same controls as `--native-auto-*` flags. + Within the automatic native route, bounded ordinary Integer/Binary linear models can use three additional transformations. The original model first passes native structural and arithmetic admission; reductions cannot turn an unsupported input diff --git a/docs/solver-parity/README.md b/docs/solver-parity/README.md index 300a7eaef7..c55289b5b9 100644 --- a/docs/solver-parity/README.md +++ b/docs/solver-parity/README.md @@ -23,7 +23,9 @@ symmetry and compact knapsack DP now extend this policy. The separate C++ `solve_native_race` option tries this policy and ordinary BAB under one shared budget, then selects a route. Exploration/restarting may increase CPU work or solve time; longer trials can pay off if they discover a better search strategy. -MiniZinc exposure and parallel racing remain future work. The final three-cohort +The experimental [MiniZinc registration](MINIZINC.md) now exposes automatic, +racing and explicitly configured native strategies. Parallel racing remains +future work. The final three-cohort benchmark compares the original pre-algorithm runtime, automatic racing and frozen family presets; the earlier studies below keep their own observations. diff --git a/doxygen/optimize.hh b/doxygen/optimize.hh index 44cb97be20..9a8222cc9c 100644 --- a/doxygen/optimize.hh +++ b/doxygen/optimize.hh @@ -44,7 +44,7 @@ * | Existing Space, IntVar, BoolVar, SetVar, FloatVar and native search APIs | The original CP modeling, global constraints, propagators, search customization and configured parallel search | Optimize restrictions below do not remove these existing capabilities. See \ref TaskModel and \ref TaskModelSearch. | * | Optimize with Backend::Highs | Numerical continuous LP and mixed-integer linear models, including supported binary and semi domains | One worker per solve; numerical tolerances and adapter scaling limits apply. Exact and Certified requests are rejected. | * | Optimize with Backend::Native | Finite Integer, Binary and SemiInteger models with exact integral linear data, retained indicators and six typed global families | Conservative native coefficient/activity limits; one deterministic worker; no arbitrary continuous or fractional model conversion. | - * | Explicit native LP/frontier/neighborhood APIs | Checked integer LP deductions, optional original-row root covers, frontier bounds, binary reliability probes and one bounded incumbent neighborhood | Explicit entry points allow direct control; the common Native policy can select LP, covers and reliability structurally. No automatic portfolio is implemented. | + * | Explicit native LP/frontier/neighborhood APIs | Checked integer LP deductions, optional original-row root covers, frontier bounds, binary reliability probes and one bounded incumbent neighborhood | Explicit entry points allow direct control; the common Native policy selects suitable LP, covers and reliability. An optional sequential race compares automatic and ordinary search. | * | QuadraticModel and solve_quadratic | Bounded continuous convex minimization or concave maximization expressed as weighted squares plus linear terms | Numerical checking; separate model type. No integer QP, quadratic constraints or general nonconvex optimization. | * * Gecode::Optimize::solve selects native %Gecode for active typed globals under @@ -60,7 +60,8 @@ * compares automatic and ordinary routes with sequential probes, then restarts * the selected route under the same time/node budget. Exploration can increase * CPU work and solve time, but can reveal a better strategy for a longer solve. - * Exploration time is configurable; MiniZinc exposure is future work. + * Exploration time is configurable. The experimental MiniZinc registration + * exposes automatic, racing and explicitly configured native strategies. * No conflict learning is added. Inspect * Gecode::Optimize::capabilities, Gecode::Optimize::native_capabilities, * Gecode::Optimize::native_lp_capabilities and @@ -365,6 +366,17 @@ * limit, whereas the direct --time-limit 0 option requests an immediate limit. * Ordinary incomplete MiniZinc output uses protocol status and exit zero; * malformed/unsupported inputs remain errors. + * Namespaced --native-* extra flags expose automatic feature switches, + * sequential racing, checked LP/cover cuts, frontier order, reliability + * branching and bounded Hamming neighborhoods. --native-diagnostics on reports + * requested settings, actual route and available work counters as comments. + * NativeAutoOptions and solve_native_auto_configured expose the same automatic + * switches to C++; NativeRaceOptions::automatic controls its automatic candidate. + * Integer 0..1 source domains retain integer output while becoming internal + * binary decisions. Bounded automatic presolve can eliminate a singly defined + * affine objective auxiliary, preserving its bounds and restoring/checking + * its original value before publication. Numerical MiniZinc model support and + * general solve annotations remain outside this registration's scope. * * \section OptimizeBindings C and Python * diff --git a/gecode/optimize/flatzinc.cpp b/gecode/optimize/flatzinc.cpp index 268168e31e..ee21b15b68 100644 --- a/gecode/optimize/flatzinc.cpp +++ b/gecode/optimize/flatzinc.cpp @@ -302,7 +302,11 @@ struct FlatZincCompiler { auto& d=domains[i];const auto& v=source.raw_variables[i];d.finish(meter); if(!d.lower||!d.upper)unsupported("FlatZinc integer variable has no finite explicit domain"); const auto lo=d.empty?0:*d.lower,hi=d.empty?0:*d.upper; - handles[i]=model.add_variable(v.reference.type==F::Type::Boolean?VariableType::Binary:VariableType::Integer,number(lo),number(hi),v.name); + // MiniZinc commonly emits binary decisions as integer 0..1 declarations. + // Retain their source integer type in the owning records/output mapping, + // while exposing the equivalent binary domain to native heuristics. + const bool binary=v.reference.type==F::Type::Boolean || (!d.empty && lo>=0 && hi<=1); + handles[i]=model.add_variable(binary?VariableType::Binary:VariableType::Integer,number(lo),number(hi),v.name); ++variables; if(d.empty)post({},1,1); else if(d.members) { diff --git a/gecode/optimize/native.cpp b/gecode/optimize/native.cpp index cafaf7d10d..10b1ad7054 100644 --- a/gecode/optimize/native.cpp +++ b/gecode/optimize/native.cpp @@ -1063,7 +1063,8 @@ namespace { SolveResult solve_native_impl(const ModelSnapshot& model, const SolveOptions& options, const NativeLpOptions* lp_options, NativeLpStatistics* lp_statistics, - const SolveBudget* inherited_budget = nullptr) { + const SolveBudget* inherited_budget = nullptr, + [[maybe_unused]] bool root_knapsack = true) { const auto started = std::chrono::steady_clock::now(); SolveResult result; result.model_id = model.model_id; result.revision = model.revision; @@ -1125,7 +1126,8 @@ SolveResult solve_native_impl(const ModelSnapshot& model, const SolveOptions& op Search::Options search_options; search_options.threads = 1; search_options.clone = true; search_options.stop = &stop; if (start_cost) start_checkpoint(budget, "start_root_alloc"); - auto root = std::make_unique(compiled, budget, nullptr, !lp_options); + auto root = std::make_unique(compiled, budget, nullptr, + root_knapsack && !lp_options); if (start_cost) start_cutoff(*root, *start_cost, budget); checkpoint(budget); BAB search(root.get(), search_options); @@ -2141,13 +2143,14 @@ struct AutomaticNativeSelection { }; AutomaticNativeSelection select_native_route(const ModelSnapshot& model, - const SolveOptions& options, const SolveBudget& budget) { + const SolveOptions& options, const SolveBudget& budget, + const NativeAutoSettings& settings) { // Optional routes must never change acceptance of an explicit native option. if ((options.backend != Backend::Auto && options.backend != Backend::Native) || options.guarantee == Guarantee::Certified || options.threads != 1 || options.random_seed != 0) return {AutomaticNativeRoute::Native,"native option compatibility"}; -#ifndef GECODE_OPTIMIZE_NATIVE_LP_ENABLED - (void)model; (void)budget; +#ifndef GECODE_OPTIMIZE_WITH_NATIVE + (void)model; (void)budget; (void)settings; return {AutomaticNativeRoute::Native,"checked LP unavailable"}; #else // Bound selection's extra work before calling the full native validator or @@ -2179,8 +2182,11 @@ AutomaticNativeSelection select_native_route(const ModelSnapshot& model, const auto compiled = compile(model,budget); if (!compiled.binary_domains || compiled.rows.empty()) return {AutomaticNativeRoute::Native,"binary domain or row structure"}; - if (prepare_knapsack(compiled,budget)) + if (settings.knapsack && prepare_knapsack(compiled,budget)) return {AutomaticNativeRoute::Native,"eligible exact knapsack DP"}; +#ifndef GECODE_OPTIMIZE_NATIVE_LP_ENABLED + return {AutomaticNativeRoute::Native,"checked LP unavailable"}; +#else // Use the same checked-LP numeric admission as the explicit LP API, without // constructing an LP backend or solving a relaxation during selection. try { (void)relaxation_model(compiled,budget); } @@ -2201,18 +2207,19 @@ AutomaticNativeSelection select_native_route(const ModelSnapshot& model, return {AutomaticNativeRoute::UpdatedLp,"updated checked LP with covers; gap-compatible BAB",true}; return {AutomaticNativeRoute::ReliabilityLp,"updated checked LP, covers and binary reliability",true}; #endif +#endif } SolveResult native_auto_impl(const ModelSnapshot& model, const SolveOptions& options, - SolveBudget& budget) { + SolveBudget& budget, const NativeAutoSettings& settings) { SolveResult result; result.model_id=model.model_id; result.revision=model.revision; result.backend="Gecode native"; result.guarantee=options.guarantee; AutomaticNativeSelection selected; try { - selected=select_native_route(model,options,budget); + selected=select_native_route(model,options,budget,settings); if (selected.route == AutomaticNativeRoute::Native) { - result=solve_native_impl(model,options,nullptr,nullptr,&budget); + result=solve_native_impl(model,options,nullptr,nullptr,&budget,settings.knapsack); } else { NativeLpOptions lp; lp.solve=options; if (selected.route != AutomaticNativeRoute::RootLp) { @@ -2238,7 +2245,7 @@ SolveResult native_auto_impl(const ModelSnapshot& model, const SolveOptions& opt // observes a stop before reaching validate_structure. No search can start // because the same exhausted/cancelled budget reaches the native bridge. (void)error; - result=solve_native_impl(model,options,nullptr,nullptr,&budget); + result=solve_native_impl(model,options,nullptr,nullptr,&budget,settings.knapsack); } catch (const Unsupported& error) { result.termination=Termination::Unsupported; result.message=error.what(); } catch (const ModelError& error) { @@ -2260,12 +2267,13 @@ SolveResult native_auto_impl(const ModelSnapshot& model, const SolveOptions& opt // Transformations are internal and single-pass. Explicit native APIs retain // their original behavior; all callbacks keep the same global budget. SolveResult native_auto_pipeline(const ModelSnapshot& model, const SolveOptions& options, - SolveBudget& budget) { + SolveBudget& budget, const NativeAutoSettings& settings) { #ifndef GECODE_OPTIMIZE_WITH_NATIVE - return native_auto_impl(model,options,budget); + return native_auto_impl(model,options,budget,settings); #else - const auto fallback=[&]{return native_auto_impl(model,options,budget);}; - if (!options.primal_start.empty() || options.guarantee==Guarantee::Certified || + const auto fallback=[&]{return native_auto_impl(model,options,budget,settings);}; + if ((!settings.presolve && !settings.components && !settings.symmetry) || + !options.primal_start.empty() || options.guarantee==Guarantee::Certified || (options.backend!=Backend::Auto && options.backend!=Backend::Native) || options.threads!=1 || options.random_seed!=0 || !model.globals.empty() || !model.indicators.empty() || @@ -2283,14 +2291,15 @@ SolveResult native_auto_pipeline(const ModelSnapshot& model, const SolveOptions& // could erase an unsupported term or contradiction. validate_structure(model);checkpoint(budget); const auto compiled=compile(model,budget); - if(prepare_knapsack(compiled,budget))return fallback(); - const Detail::NativeSolveContinuation leaf=[](const ModelSnapshot& m, - const SolveOptions& o,SolveBudget& b){return native_auto_impl(m,o,b);}; + if(settings.knapsack && prepare_knapsack(compiled,budget))return fallback(); + const Detail::NativeSolveContinuation leaf=[&](const ModelSnapshot& m, + const SolveOptions& o,SolveBudget& b){return native_auto_impl(m,o,b,settings);}; const Detail::NativeSolveContinuation symmetric=[&](const ModelSnapshot& m, const SolveOptions& o,SolveBudget& b){ + if(!settings.symmetry)return leaf(m,o,b); // A reduced/component model can itself become a DP candidate. try { - if(prepare_knapsack(compile(m,b),b))return leaf(m,o,b); + if(settings.knapsack && prepare_knapsack(compile(m,b),b))return leaf(m,o,b); } catch(const Unsupported&) { // Let the ordinary leaf report admission rather than throwing through // the presolve coordinator, which can then retain the original model. @@ -2301,11 +2310,19 @@ SolveResult native_auto_pipeline(const ModelSnapshot& model, const SolveOptions& }; const Detail::NativeSolveContinuation components=[&](const ModelSnapshot& m, const SolveOptions& o,SolveBudget& b){ - if(auto result=Detail::native_components(m,o,b,symmetric))return *result; + if(settings.components) + if(auto result=Detail::native_components(m,o,b,symmetric))return *result; return symmetric(m,o,b); }; - auto result=Detail::native_presolve(model,options,budget,components); - auto solved=result ? std::move(*result):components(model,options,budget); + const Detail::NativeSolveContinuation presolved=[&](const ModelSnapshot& m, + const SolveOptions& o,SolveBudget& b){ + if(settings.presolve) + if(auto result=Detail::native_presolve(m,o,b,components))return *result; + return components(m,o,b); + }; + auto normalized=settings.presolve ? Detail::native_objective_auxiliary(model,options,budget,presolved): + std::optional{}; + auto solved=normalized ? std::move(*normalized):presolved(model,options,budget); solved.message="Automatic native policy: preprocessing; "+solved.message; solved.elapsed_seconds=budget.elapsed_seconds(); return solved; @@ -2324,15 +2341,15 @@ SolveResult native_auto_pipeline(const ModelSnapshot& model, const SolveOptions& template SolveResult native_auto_entry(const Source& source, const SolveOptions& options, - ModelId id, Revision revision) { + const NativeAutoSettings& settings, ModelId id, Revision revision) { const auto started=std::chrono::steady_clock::now(); SolveResult result; result.model_id=id; result.revision=revision; result.backend="Gecode native"; result.guarantee=options.guarantee; try { SolveBudget budget(options); if constexpr (std::is_same_v) - result=native_auto_pipeline(source.snapshot(),options,budget); - else result=native_auto_pipeline(source,options,budget); + result=native_auto_pipeline(source.snapshot(),options,budget,settings); + else result=native_auto_pipeline(source,options,budget,settings); // Include transformation/artifact cleanup in the publication deadline. // Ordinary timed incumbents and the explicit-start path retain their existing // capture semantics; a newly completed preprocessing proof must be timely. @@ -2357,10 +2374,17 @@ SolveResult native_auto_entry(const Source& source, const SolveOptions& options, } SolveResult solve_native_auto(const ModelSnapshot& model, const SolveOptions& options) { - return native_auto_entry(model,options,model.model_id,model.revision); + return native_auto_entry(model,options,{},model.model_id,model.revision); } SolveResult solve_native_auto(const Model& model, const SolveOptions& options) { - return native_auto_entry(model,options,model.id(),model.revision()); + return native_auto_entry(model,options,{},model.id(),model.revision()); +} + +SolveResult solve_native_auto_configured(const ModelSnapshot& model, const NativeAutoOptions& options) { + return native_auto_entry(model,options.solve,options.settings,model.model_id,model.revision); +} +SolveResult solve_native_auto_configured(const Model& model, const NativeAutoOptions& options) { + return native_auto_entry(model,options.solve,options.settings,model.id(),model.revision()); } void NativeRaceOptions::validate() const { @@ -2381,7 +2405,7 @@ SolveResult native_race_impl(const ModelSnapshot& model,const NativeRaceOptions& solve.guarantee==Guarantee::Certified || solve.threads!=1 || solve.random_seed!=0 || (solve.backend!=Backend::Auto && solve.backend!=Backend::Native) || !native_capabilities().available) { - auto result=native_auto_pipeline(model,solve,budget); + auto result=native_auto_pipeline(model,solve,budget,options.automatic); result.message="Native race skipped (disabled or direct-path compatibility); "+result.message; return result; } @@ -2400,7 +2424,7 @@ SolveResult native_race_impl(const ModelSnapshot& model,const NativeRaceOptions& (!bound || better_bound(*result.best_bound,*bound)))bound=result.best_bound; }; const auto run=[&](bool automatic,SolveBudget& allowance){ - auto result=automatic ? native_auto_pipeline(model,solve,allowance): + auto result=automatic ? native_auto_pipeline(model,solve,allowance,options.automatic): solve_native_impl(model,solve,nullptr,nullptr,&allowance); // A completed proof is only published after destruction of candidate-local // artifacts. Reaching a node cap on the final admitted node is permitted. diff --git a/gecode/optimize/native.hpp b/gecode/optimize/native.hpp index 6839a1cc51..85ffa0f263 100644 --- a/gecode/optimize/native.hpp +++ b/gecode/optimize/native.hpp @@ -42,12 +42,40 @@ SolveResult solve_native_auto(const ModelSnapshot& model, SolveResult solve_native_auto(const Model& model, const SolveOptions& options = {}); +/** Optional automatic transformations. Disabling a feature skips its work; + * enabling it permits the conservative structural policy to use it when safe. + * These controls apply throughout reduced models and independent components. + * They do not change the behavior of explicit solve_native/LP/search APIs. + */ +struct NativeAutoSettings { + /** Exact reductions, including one safely reconstructable affine objective + * auxiliary (for example a MiniZinc compiler-generated objective variable). + */ + bool presolve = true; + bool components = true; + bool symmetry = true; + bool knapsack = true; +}; + +struct NativeAutoOptions { + SolveOptions solve; + NativeAutoSettings settings; +}; + +/** Run the automatic policy with explicit transformation controls. A separate + * name preserves unambiguous existing calls such as solve_native_auto(model,{}). + */ +SolveResult solve_native_auto_configured(const ModelSnapshot& model, + const NativeAutoOptions& options = {}); +SolveResult solve_native_auto_configured(const Model& model, + const NativeAutoOptions& options = {}); + /** Opt-in sequential probe-and-select policy for native Gecode optimization. * Racing can INCREASE total CPU work and solve time: probes and restarting the * selected strategy repeat work. Several seconds (or longer when configured) * can nevertheless discover a substantially better search route. Early progress * is a heuristic, not a prediction or a guarantee of eventual speedup. - * No MiniZinc/FlatZinc option is exposed by this C++ entry point yet. + * The optional Optimize MiniZinc/FlatZinc frontend exposes this policy separately. */ struct NativeRaceOptions { SolveOptions solve; @@ -59,11 +87,16 @@ struct NativeRaceOptions { double exploration_seconds = 2.0; /** Per-probe node allowance; all probe/restart nodes also count globally. */ std::uint64_t probe_node_limit = 4096; + /** Controls only the automatic candidate, including a selected restart or + * direct-path fallback. The ordinary native comparator retains its existing + * eligible exact knapsack DP, independently of these settings. + */ + NativeAutoSettings automatic; void validate() const; }; /** Compare automatic preprocessing/LP policy with ordinary native BAB, preserving - * eligible exact knapsack DP in both. Return immediately on a complete proof; + * eligible exact knapsack DP by default in both. Return immediately on a complete proof; * otherwise restart the candidate with the best original validated incumbent, * then strongest valid bound, preferring automatic policy on ties. Validated * incumbents and original-model bounds from probes are retained. Search trees diff --git a/gecode/optimize/native_preprocess.hpp b/gecode/optimize/native_preprocess.hpp index cf18ed5f8a..f2a9aa8562 100644 --- a/gecode/optimize/native_preprocess.hpp +++ b/gecode/optimize/native_preprocess.hpp @@ -9,6 +9,9 @@ using NativeSolveContinuation = std::function; std::optional native_presolve(const ModelSnapshot&, const SolveOptions&, SolveBudget&, const NativeSolveContinuation&); +/** Eliminate one singleton affine objective auxiliary after native admission. */ +std::optional native_objective_auxiliary(const ModelSnapshot&, const SolveOptions&, + SolveBudget&, const NativeSolveContinuation&); std::optional native_components(const ModelSnapshot&, const SolveOptions&, SolveBudget&, const NativeSolveContinuation&); std::optional native_symmetry(const ModelSnapshot&, const SolveOptions&, diff --git a/gecode/optimize/native_presolve.cpp b/gecode/optimize/native_presolve.cpp index 22ae693a3d..f322c86036 100644 --- a/gecode/optimize/native_presolve.cpp +++ b/gecode/optimize/native_presolve.cpp @@ -1,7 +1,9 @@ /* Exact, bounded presolve composition for the automatic native coordinator. */ #include #include +#include +#include #include #include #include @@ -24,6 +26,130 @@ SolveResult original_result(const ModelSnapshot& model, const SolveOptions& opti } } +std::optional native_objective_auxiliary(const ModelSnapshot& model, + const SolveOptions& options, SolveBudget& budget, + const NativeSolveContinuation& continuation) { + // A single exact equality can hide a binary objective behind a nonbinary + // FlatZinc auxiliary. This is one bounded substitution, never recursive + // algebra or an assumption that a name/annotation implies equivalence. + if (!options.primal_start.empty() || options.guarantee==Guarantee::Certified || + (options.backend!=Backend::Auto && options.backend!=Backend::Native) || + options.threads!=1 || options.random_seed!=0 || + !model.globals.empty() || !model.indicators.empty() || + model.variables.size()>4096 || model.rows.size()>4096 || + model.objective.terms.size()!=1 || model.objective.terms[0].coefficient!=1) return {}; + auto result=original_result(model,options); + const auto finish=[&](SolveResult value) -> std::optional { + if(const auto stop=deadline_stop(budget)) { + value=original_result(model,options);value.termination=*stop; + value.message="Exact objective auxiliary substitution stopped before original-result publication"; + } + value.elapsed_seconds=budget.elapsed_seconds();return value; + }; + try { + if(const auto stop=budget.stop_reason()) {result.termination=*stop;return finish(std::move(result));} + validate_structure(model); + const auto auxiliary=model.objective.terms[0].variable.id; + const auto& variable=model.variables[auxiliary]; + if(variable.type!=VariableType::Integer || + (variable.lower>=0 && variable.upper<=1)) return {}; + // Independently bound every conversion/product below, even though callers + // have already compiled the original model under stricter native limits. + constexpr std::int64_t limit=INT64_C(2147483647), exact=INT64_C(9007199254740992); + const auto integer=[](double value) { + return std::isfinite(value) && std::trunc(value)==value && std::abs(value)<=2147483647.0; + }; + for(const auto& v:model.variables) if(v.active && + ((v.type!=VariableType::Integer && v.type!=VariableType::Binary) || + !integer(v.lower) || !integer(v.upper))) return {}; + std::optional equality; + double sign=0;std::size_t nonzeros=0; + for(std::size_t i=0;i65536-nonzeros)return {};nonzeros+=row.terms.size(); + if(!row.active)continue; + for(const auto& term:row.terms) if(term.variable.id==auxiliary) { + if(equality || row.lower!=row.upper || !integer(row.lower) || + std::abs(term.coefficient)!=1)return {}; + equality=i;sign=term.coefficient; + } + } + if(!equality)return {}; + const auto& equation=model.rows[*equality]; + const auto constant=static_cast(sign*equation.lower); + std::int64_t lower=constant,upper=constant,magnitude=0; + std::vector terms; + for(const auto& term:equation.terms) if(term.variable.id!=auxiliary) { + if(!integer(term.coefficient))return {}; + const auto coefficient=static_cast(-sign*term.coefficient); + const auto& v=model.variables[term.variable.id]; + const auto a=coefficient*static_cast(v.lower); + const auto b=coefficient*static_cast(v.upper); + const auto size=std::max(std::abs(a),std::abs(b)); + if(size>limit-magnitude)return {};magnitude+=size; + lower+=std::min(a,b);upper+=std::max(a,b); + terms.push_back({term.variable,static_cast(coefficient)}); + } + if(!std::isfinite(model.objective.offset) || std::trunc(model.objective.offset)!=model.objective.offset || + std::abs(model.objective.offset)>static_cast(exact))return {}; + const auto offset=static_cast(model.objective.offset); + if(std::abs(offset+constant)>exact || std::abs(offset+lower)>exact || std::abs(offset+upper)>exact)return {}; + auto reduced=model;reduced.variables[auxiliary].active=false; + reduced.objective.terms=terms;reduced.objective.offset=static_cast(offset+constant); + auto& row=reduced.rows[*equality]; + row.terms=terms;row.lower=variable.lower-constant;row.upper=variable.upper-constant; + // Auxiliary domain bounds are real constraints. Remove the defining row + // only when the remaining variable domain box independently implies both. + if(lower>=variable.lower && upper<=variable.upper){row.active=false;row.terms.clear();} + validate_structure(reduced); + auto exact_options=options;exact_options.guarantee=Guarantee::Exact; + auto solved=continuation(reduced,exact_options,budget); + if(const auto stop=deadline_stop(budget)){result.termination=*stop;return finish(std::move(result));} + if(solved.model_id!=reduced.model_id || solved.revision!=reduced.revision || + solved.guarantee!=Guarantee::Exact || solved.start_submitted) + throw std::runtime_error("Objective auxiliary solve returned foreign identity, guarantee or start"); + if(solved.termination==Termination::Unsupported)return {}; // Preserve original numeric admission. + if(solved.termination==Termination::InvalidModel || solved.termination==Termination::Unbounded || + solved.termination==Termination::InfeasibleOrUnbounded || + (solved.best_bound && !std::isfinite(*solved.best_bound))) + throw std::runtime_error("Objective auxiliary solve returned inconsistent status or bound"); + if(solved.has_solution()) { + if(solved.values.size()!=model.variables.size() || solved.active_variables.size()!=model.variables.size()) + throw std::runtime_error("Objective auxiliary solve returned incomplete coordinates"); + for(std::size_t i=0;i(term.coefficient)* + static_cast(solved.values[term.variable.id]); + solved.values[auxiliary]=static_cast(value);solved.active_variables[auxiliary]=true; + const auto restored=validate(model,solved.values,0,0); + if(!restored.valid || restored.objective!=solved.objective) + throw std::runtime_error("Objective auxiliary original witness failed exact validation"); + solved.solution_validated=true; + } + if((solved.termination==Termination::Optimal && !solved.has_solution()) || + (solved.termination==Termination::Infeasible && solved.has_solution())) + throw std::runtime_error("Objective auxiliary solve returned inconsistent proof status"); + // Full objectives (including the constant) are equal, so original bounds + // transfer unchanged. No transformed point/proof is published before QA. + solved.guarantee=options.guarantee;solved.update_gaps(model.objective.sense); + solved.message="Exact objective auxiliary substitution; "+solved.message; + return finish(std::move(solved)); + } catch(const std::bad_alloc&) { + result=original_result(model,options);result.termination=Termination::MemoryLimit; + result.message="Exact objective auxiliary substitution allocation failed"; + } catch(const std::exception& error) { + result=original_result(model,options);result.termination=Termination::BackendError; + result.message=std::string("Exact objective auxiliary substitution: ")+error.what(); + } + return finish(std::move(result)); +} + std::optional native_presolve(const ModelSnapshot& model, const SolveOptions& options, SolveBudget& budget, const NativeSolveContinuation& continuation) { diff --git a/test/optimize/flatzinc.cpp b/test/optimize/flatzinc.cpp index f3f0761ce1..a2e675fd96 100644 --- a/test/optimize/flatzinc.cpp +++ b/test/optimize/flatzinc.cpp @@ -92,6 +92,20 @@ void booleans(){ oracle(channel,{{0,1},{-1,2}},[](const Point& p){return 2*p[0]-1==p[1];}); } void aliases_domains(){ + // Domain-based binary recognition must not change source typing, aliases, + // singleton restrictions, or acceptance of assignments outside the domain. + F::Records binary;binary.raw_variables={variable(0,0,1),variable(1,-2,3),variable(2,1,1),variable(3,0,2)}; + binary.raw_variables[1].alias=true;binary.raw_variables[1].target={F::Type::Integer,0}; + binary.output={{"integer_decision",ref(0)}}; + const auto classified=compiled(binary); + assert(classified.model().variables[0].type==O::VariableType::Binary); + assert(classified.variables()[0].variable==classified.variables()[1].variable); + assert(classified.model().variables[1].type==O::VariableType::Binary); + assert(classified.model().variables[2].type==O::VariableType::Integer); + assert(O::format_flatzinc_solution(classified,witness(classified,{1,1,1,2}))=="integer_decision = 1;\n----------\n"); + oracle(binary,{{-1,2},{-1,2},{0,2},{-1,3}},[](const Point& p){ + return p[0]>=0&&p[0]<=1&&p[0]==p[1]&&p[2]==1&&p[3]>=0&&p[3]<=2; + }); F::Records r;r.raw_variables={variable(0,-2,3),variable(1,-9,9),variable(2,-9,9)}; r.raw_variables[1].alias=true;r.raw_variables[1].target={F::Type::Integer,0};r.raw_variables[2].alias=true;r.raw_variables[2].target={F::Type::Integer,1}; r.raw_domains={row("int_in",{ref(1),domain(0,2)})}; diff --git a/test/optimize/flatzinc_driver.cpp b/test/optimize/flatzinc_driver.cpp index 35acd0a0a4..4f89ef55f8 100644 --- a/test/optimize/flatzinc_driver.cpp +++ b/test/optimize/flatzinc_driver.cpp @@ -5,8 +5,8 @@ namespace FznOptimizeDriver { int fake=0,calls=0; -O::SolveResult test_solve(const O::ModelSnapshot& m,const O::SolveOptions& options) { - ++calls;if(!fake)return O::solve(m,options); +SolveOutput test_solve(const O::ModelSnapshot& m,const Options& controls,const O::SolveOptions& options) { + ++calls;if(!fake)return dispatch(m,controls,options); O::SolveResult r;r.model_id=m.model_id;r.revision=m.revision;r.guarantee=options.guarantee; r.termination=O::Termination::Optimal;r.values.resize(m.variables.size(),0); r.active_variables.resize(m.variables.size(),true);r.solution_validated=true;r.objective=0; @@ -34,9 +34,10 @@ O::SolveResult test_solve(const O::ModelSnapshot& m,const O::SolveOptions& optio case 20:r.absolute_gap=std::numeric_limits::quiet_NaN();break; case 21:r.relative_gap=1;break; case 22:r.termination=O::Termination::Infeasible;clear();r.objective=std::numeric_limits::quiet_NaN();break; + case 23:r.backend="native\r\n=====UNSATISFIABLE=====";r.message="policy\n==========\tmessage";break; default:break; } - return r; + return {r,fake==23?"counter\n=====UNKNOWN=====":""}; } } using namespace FznOptimizeDriver; @@ -62,6 +63,63 @@ void rejected_arguments() { auto valid=arguments({"-","--backend","highs","--time-limit","1e2","--node-limit","18446744073709551615"}); assert(valid.solve.time_limit_seconds==100&&valid.solve.node_limit==std::numeric_limits::max());++checks; } +void native_arguments() { + const std::vector> invalid={ + {"--native-mode","unknown"},{"--native-mode"}, + {"--native-diagnostics","true"},{"--native-unknown","on"}, + {"--native-mode","auto","--native-mode","auto"}, + {"--native-node-limit","1","--node-limit","2"}, + {"--node-limit","1","--native-node-limit","2"}, + {"--backend","highs","--native-mode","auto"}, + {"--backend","highs","--native-diagnostics","off"}, + {"--native-mode","plain","--native-auto-knapsack","off"}, + {"--native-auto-presolve","true"},{"--native-race-seconds","2"}, + {"--native-mode","race","--native-race-seconds","nan"}, + {"--native-mode","race","--native-race-seconds","-1"}, + {"--native-mode","race","--native-race-nodes","0"}, + {"--native-mode","race","--native-race-nodes","18446744073709551616"}, + {"--native-lp","root"},{"--native-mode","configured","--native-lp","bad"}, + {"--native-mode","configured","--native-root-cuts","on"}, + {"--native-mode","configured","--native-bound-tightening","off"}, + {"--native-mode","configured","--native-lp","root","--native-lp-interval","2"}, + {"--native-mode","configured","--native-lp","updated","--native-lp-interval","0"}, + {"--native-mode","configured","--native-lp","updated","--native-lp-interval","4294967296"}, + {"--native-mode","configured","--native-search","bab","--native-branching","default"}, + {"--native-mode","configured","--native-search","bab","--native-max-open-nodes","1"}, + {"--native-mode","configured","--native-search","bab","--native-neighborhood","off"}, + {"--native-mode","configured","--native-branching-probes","1"}, + {"--native-mode","configured","--native-neighborhood-radius","1"}, + {"--native-mode","configured","--native-neighborhood-nodes","1"}, + {"--native-mode","configured","--native-neighborhood-seconds","1"}, + {"--native-mode","configured","--native-neighborhood","hamming","--native-neighborhood-seconds","inf"}, + {"--native-mode","configured","--native-max-open-nodes","18446744073709551616"} + }; + for(auto args:invalid) { + args.insert(args.begin(),"m");bool threw=false; + try{arguments(args);}catch(const std::invalid_argument&){threw=true;}assert(threw);++checks; + // Native-prefixed controls use identical validation in the MiniZinc protocol. + args.insert(args.begin(),"--minizinc");threw=false; + try{arguments(args);}catch(const std::invalid_argument&){threw=true;}assert(threw);++checks; + } + auto automatic=arguments({"--minizinc","--native-auto-presolve","off","-t","1000","m", + "--native-auto-components","off","--native-auto-symmetry","off","--native-auto-knapsack","off"}); + assert(!automatic.automatic.presolve&&!automatic.automatic.components&&!automatic.automatic.symmetry&&!automatic.automatic.knapsack); + assert(automatic.solve.time_limit_seconds==1&&automatic.filename=="m");++checks; + auto race=arguments({"m","--native-mode","race","--native-race-seconds","0","--native-race-nodes","1"}); + assert(race.race.exploration_seconds==0&&race.race.probe_node_limit==1);++checks; + auto configured=arguments({"--minizinc","m","--native-mode","configured","--native-search","best-bound", + "--native-lp","updated","--native-lp-interval","7","--native-root-cuts","on","--native-bound-tightening","off", + "--native-branching","reliability","--native-branching-probes","19","--native-max-open-nodes","50", + "--native-neighborhood","hamming","--native-neighborhood-radius","2","--native-neighborhood-nodes","17", + "--native-neighborhood-seconds","0.25","--native-node-limit","99","--native-diagnostics","on"}); + const auto search=search_options(configured,configured.solve); + assert(search.order==O::NativeSearchOrder::BestBound&&search.relaxation&&search.relaxation->root_cover_cuts); + assert(!search.relaxation->bound_tightening&&search.relaxation->bound_change_interval==7); + assert(search.relaxation->frequency==O::NativeLpFrequency::AfterBoundChanges&&search.branching&& + search.branching->max_probe_status_calls==19&&search.max_open_nodes==50); + assert(configured.neighborhood_settings.radius==2&&configured.neighborhood_settings.max_status_calls==17&& + configured.neighborhood_settings.time_limit_seconds==0.25&&configured.solve.node_limit==99&&configured.diagnostics);++checks; +} void fake_contract() { for(fake=1;fake<=22;++fake) { auto result=run(basic); @@ -92,8 +150,39 @@ void fake_contract() { assert(holes.first==0&&calls==1&&holes.second.find("x = 0;")!=std::string::npos); calls=0; assert(run("var {-1,1}: x :: output_var; solve minimize x;").first==2&&calls==1); + fake=23;Options diagnostic;diagnostic.diagnostics=true; + auto escaped=run(basic,diagnostic);assert(escaped.first==0); + assert(escaped.second.find("\n=====UNSATISFIABLE=====")==std::string::npos&& + escaped.second.find("\n=====UNKNOWN=====")==std::string::npos&& + escaped.second.find("% native-backend: native =====UNSATISFIABLE=====\n")!=std::string::npos&& + escaped.second.find("% native-policy: policy ========== message\n")!=std::string::npos); fake=0; } +void actual_native_controls() { + for(const auto& mode:{"auto","plain","race","configured"}) { + auto o=arguments({"m","--native-mode",mode,"--native-diagnostics","on"}); + auto solved=run(basic,o); + if(!O::native_capabilities().available) {assert(solved.first==2);continue;} + assert(solved.first==0&&solved.second.find(std::string("% native-mode: ")+mode+"\n")!=std::string::npos&& + solved.second.find("x = 0;\n----------\n==========\n")!=std::string::npos); + if(std::string(mode)=="configured")assert(solved.second.find("native frontier")!=std::string::npos); + } + for(const auto& order:{"bab","dfs","best-bound"})for(const auto& lp:{"off","root","updated"}) { + std::vector args={"m","--native-mode","configured","--native-search",order,"--native-lp",lp,"--native-diagnostics","on"}; + if(std::string(lp)!="off")args.insert(args.end(),{"--native-root-cuts","on"}); + if(std::string(order)!="bab")args.insert(args.end(),{"--native-branching","reliability","--native-neighborhood","hamming"}); + auto solved=run(basic,arguments(args)); + if(!O::native_capabilities().available||(std::string(lp)!="off"&&!O::native_lp_capabilities().available)) { + assert(solved.first==2);continue; + } + assert(solved.first==0&&solved.second.find("x = 0;")!=std::string::npos); + if(std::string(lp)!="off")assert(solved.second.find("checked LP")!=std::string::npos&&solved.second.find("lp-calls=")!=std::string::npos); + if(std::string(order)!="bab")assert(solved.second.find("branching-probes=")!=std::string::npos&&solved.second.find("neighborhood-attempts=")!=std::string::npos); + } + auto zero=arguments({"--minizinc","m","--native-mode","race","--native-node-limit","0","--native-diagnostics","on"}); + auto stopped=run(basic,zero); + if(O::native_capabilities().available)assert(stopped.first==0&&stopped.second.find("=====UNKNOWN=====")!=std::string::npos&&stopped.second.find("x =")==std::string::npos); +} void actual_pipeline() { int available=0; for(auto backend:{O::Backend::Native,O::Backend::Highs}) { @@ -126,4 +215,4 @@ void actual_pipeline() { #endif } } -int main() {rejected_arguments();fake_contract();actual_pipeline();assert(checks>=50);std::cout<<"FlatZinc complete frontend: "<=120);std::cout<<"FlatZinc complete frontend: "< None: + # Original source oracle: two binary items of weight 2 cannot both fit + # capacity 3; z counts chosen items. No reference result is used. + source = ("var 0..1: x; var 0..1: y; var 0..2: z :: output_var; " + "constraint int_lin_le([2,2],[x,y],3); " + "constraint int_lin_eq([1,1,-1],[x,y,z],0); solve maximize z;") + routes = [ + ("auto", []), ("plain", []), + ("race", ["--native-race-seconds", "0.02", "--native-race-nodes", "2"]), + ("auto", ["--native-auto-presolve", "off", "--native-auto-components", "off", + "--native-auto-symmetry", "off", "--native-auto-knapsack", "off"]), + ("configured", ["--native-search", "bab"]), + ("configured", ["--native-search", "dfs", "--native-branching", "reliability", + "--native-branching-probes", "8", "--native-neighborhood", "hamming", + "--native-neighborhood-radius", "1", "--native-neighborhood-nodes", "8", + "--native-neighborhood-seconds", "0.02", "--native-max-open-nodes", "100"]), + ("configured", ["--native-search", "best-bound"]), + ] + for order in ("bab", "dfs", "best-bound"): + for lp in ("root", "updated"): + extra = ["--native-search", order, "--native-lp", lp, "--native-root-cuts", "on", + "--native-bound-tightening", "off"] + if lp == "updated": + extra += ["--native-lp-interval", "2"] + routes.append(("configured", extra)) + for index, (mode, extra) in enumerate(routes): + args = ["--minizinc", "--native-mode", mode, "-", "--native-diagnostics", "on", *extra] + code, stdout, stderr = self.invoke(f"native-controls-{index}", args, source.encode()) + lp_requested = "--native-lp" in extra + if lp_requested and highs == "unavailable": + require(code == 2 and not stdout and "unsupported" in stderr.lower(), + "Requested unavailable checked LP must fail explicitly") + continue + parsed = parse_output(stdout) + require(code == 0 and not stderr and parsed.assignments == {"z": 1} and + parsed.markers == ["----------", "=========="], + f"Native route {index} failed its independent source oracle: {code}, {stdout!r}, {stderr!r}") + require(f"% native-mode: {mode}" in parsed.comments, "Requested native route missing from diagnostics") + backend = next((line for line in parsed.comments if line.startswith("% native-backend: ")), "") + require("Gecode native" in backend, "Actual native backend attribution missing") + if mode == "configured" and "bab" not in extra: + require("native frontier" in backend and "frontier-admitted=" in stdout, + "Configured frontier controls did not reach the frontier solver") + if lp_requested: + require("checked LP" in backend and re.search(r"lp-calls=[1-9]\d*", stdout), + "Checked LP controls did not perform an LP attempt") + if "--native-neighborhood" in extra: + require("neighborhood-attempts=" in stdout and "branching-probes=" in stdout, + "Requested branching/neighborhood work counters missing") + if "--native-auto-presolve" in extra: + require(all(f"auto-{feature}=off" in stdout for feature in ("presolve", "components", "symmetry", "knapsack")), + "Automatic transformation flags were not forwarded") + for mode in ("auto", "plain", "race", "configured"): + code, stdout, stderr = self.invoke(f"native-controls-zero-{mode}", + ["--minizinc", "-", "--native-mode", mode, "--native-node-limit", "0"], source.encode()) + parsed = parse_output(stdout) + require(code == 0 and not parsed.assignments and parsed.markers == ["=====UNKNOWN====="], + f"Native mode {mode} ignored the shared zero node budget") + invalid = [ + ["--native-mode", "race", "--native-race-nodes", "0"], + ["--native-mode", "race", "--native-race-seconds", "nan"], + ["--native-mode", "plain", "--native-auto-presolve", "off"], + ["--native-mode", "configured", "--native-root-cuts", "on"], + ["--native-mode", "configured", "--native-neighborhood-nodes", "1"], + ["--native-mode", "configured", "--native-search", "bab", "--native-branching", "reliability"], + ["--native-mode", "configured", "--native-lp", "updated", "--native-lp-interval", "4294967296"], + ["--native-node-limit", "18446744073709551616"], + ["--native-mode", "auto", "--native-mode", "auto"], + ["--native-diagnostics", "yes"], + ] + for index, flags in enumerate(invalid): + self.error(f"native-controls-reject-{index}", ["--minizinc", "-", *flags], source) + self.error("native-controls-highs-rejected", ["-", "--backend", "highs", "--native-mode", "auto"], source, + "require the native backend") + self.error("native-controls-node-alias-duplicate", ["-", "--node-limit", "2", "--native-node-limit", "3"], source, + "repeated") + def cases(self, highs: str) -> None: # Analytic source oracles, independent of any solver result. alias = {"a": Array(((-1, 0), (2, 3)), (1, 1, 2, 3)), "y": 1} @@ -346,6 +423,7 @@ def regular(word: tuple[int, ...], states: int, symbols: int, spaced.write_bytes(default.read_bytes()) code, stdout, stderr = self.invoke("filename-with-spaces", [str(spaced)]) require(code == 0 and not stderr and parse_output(stdout).assignments == channel, "Spaced filename failed") + self.native_controls(highs) def main() -> int: @@ -361,7 +439,7 @@ def main() -> int: digest = hashlib.sha256(args.binary.read_bytes()).hexdigest() suite = Suite(args.binary.resolve(), args.fixtures.resolve(), args.timeout) suite.cases(args.highs) - require(len(suite.results) == (106 if args.highs == "available" else 97), "Required CLI cases were skipped") + require(len(suite.results) == (135 if args.highs == "available" else 126), "Required CLI cases were skipped") print(json.dumps({"status": "passed", "binary_sha256": digest, "cases": len(suite.results), "fixture_sha256": suite.sources, "checks": suite.results}, sort_keys=True)) return 0 diff --git a/test/optimize/minizinc-fixtures/mzn-native-controls.mzn b/test/optimize/minizinc-fixtures/mzn-native-controls.mzn new file mode 100644 index 0000000000..0e763c75a8 --- /dev/null +++ b/test/optimize/minizinc-fixtures/mzn-native-controls.mzn @@ -0,0 +1,11 @@ +% Multiple weighted rows avoid a single-knapsack special case. Boolean originals +% keep binary reliability and Hamming neighborhoods eligible after flattening. +array[1..6] of var bool: take; +array[1..6] of int: weight = [3,3,2,2,4,1]; +array[1..6] of int: profit = [5,4,3,3,6,1]; +constraint sum(i in 1..6)(weight[i]*bool2int(take[i])) <= 8; +constraint 3*bool2int(take[1])+3*bool2int(take[2]) <= 5; +constraint bool2int(take[3])+bool2int(take[4])+bool2int(take[5]) <= 2; +var int: value = sum(i in 1..6)(profit[i]*bool2int(take[i])); +solve maximize value; +output [show([bool2int(take[i]) | i in 1..6] ++ [value]), "\n"]; diff --git a/test/optimize/minizinc-fixtures/mzn-native-knapsack.mzn b/test/optimize/minizinc-fixtures/mzn-native-knapsack.mzn new file mode 100644 index 0000000000..d6c845907e --- /dev/null +++ b/test/optimize/minizinc-fixtures/mzn-native-knapsack.mzn @@ -0,0 +1,9 @@ +% Integer 0..1 variables and the compiler-introduced objective must reach +% automatic exact knapsack DP after the safe objective equality is eliminated. +array[1..6] of var 0..1: take; +array[1..6] of int: weight = [3,3,2,2,4,1]; +array[1..6] of int: profit = [5,4,3,3,6,1]; +constraint sum(i in 1..6)(weight[i]*take[i]) <= 8; +var int: value = sum(i in 1..6)(profit[i]*take[i]); +solve maximize value; +output [show([take[i] | i in 1..6] ++ [value]), "\n"]; diff --git a/test/optimize/minizinc_configure.py b/test/optimize/minizinc_configure.py index 059a26af46..e3623eb039 100644 --- a/test/optimize/minizinc_configure.py +++ b/test/optimize/minizinc_configure.py @@ -32,6 +32,12 @@ def main(): assert value["version"] == version assert value["executable"] == [driver,"--minizinc"] assert value["mznlib"] == library + # Generated build/install registrations retain the public controls; + # configuring paths must not erase their types, defaults or help. + expected_flags = json.loads(template.read_text())["extraFlags"] + assert value["extraFlags"] == expected_flags + assert len({flag[0] for flag in value["extraFlags"]}) == len(expected_flags) == 21 + assert value["stdFlags"] == ["-t"] assert not list(output.parent.glob(output.name+".*.tmp")) prior = output.read_bytes() for omitted in ("VERSION","DRIVER","MZNLIB","OUTPUT","TEMPLATE"): diff --git a/test/optimize/minizinc_registration.py b/test/optimize/minizinc_registration.py index 806a1ea35c..61c7cd102c 100644 --- a/test/optimize/minizinc_registration.py +++ b/test/optimize/minizinc_registration.py @@ -38,7 +38,7 @@ class Suite: def __init__(self, args, directory): self.args, self.directory = args, directory self.deadline = time.monotonic() + args.timeout - self.checks, self.sources = [], {} + self.checks, self.sources, self.native_results = [], {}, [] self.msc = args.registration or directory / "gecode-optimize.msc" if args.registration is None: config = json.loads((ROOT / "tools/flatzinc/gecode-optimize.msc.in").read_text()) @@ -191,6 +191,14 @@ def tests(s): require(configs[0]["stdFlags"] == ["-t"] and configs[0]["tags"] == ["cp","int","experimental"], "Registration overstates supported flags/types") require("default" not in configs[0]["tags"], "Experimental registration changed the default") + advertised = {flag[0]: flag for flag in configs[0]["extraFlags"]} + expected = set("mode auto-presolve auto-components auto-symmetry auto-knapsack race-seconds race-nodes lp root-cuts bound-tightening lp-interval search branching branching-probes max-open-nodes neighborhood neighborhood-radius neighborhood-nodes neighborhood-seconds node-limit diagnostics".split()) + require(set(advertised) == {"--native-"+name for name in expected}, "Missing or unexpected native controls") + require(advertised["--native-mode"][2:] == ["opt:auto:race:plain:configured", "auto"], "Wrong mode contract") + require("CPU" in advertised["--native-race-seconds"][1] and "solve time" in advertised["--native-race-seconds"][1], + "Registration must disclose race overhead") + code, stdout, stderr = s.run("solver-native-help", [s.args.minizinc, "--help", IDENTITY]) + require(code == 0 and not stderr and all(flag in stdout for flag in advertised), "Native controls absent from solver help") a = [(x,y,2*x+y-4) for x,y in itertools.product(range(4),repeat=2) if x+y >= 3] s.positive("linear-min", {min(a,key=lambda p:p[2])}) a = [(x,y,3*x-y+2) for x,y in itertools.product(range(-2,3),repeat=2) if x+y <= 1] @@ -225,6 +233,7 @@ def tests(s): ("float","float and set variables"),("set","float and set variables"),("search","search annotations"), ("variable-cumulative","original singleton")): s.rejected("reject-"+name,text) + native_controls(s) # Test flags through the actual MiniZinc parser, not only the .msc JSON. for flag in ("--all-solutions","--intermediate-solutions"): args = [flag] @@ -257,12 +266,174 @@ def tests(s): large = s.directory/"capture-deadline.fzn" large.write_text("".join(f"var 0..1: x{i};\n" for i in range(20000))+"solve satisfy;\n") for prefix in ([s.args.binary,"--minizinc","-t","1"], - [s.args.minizinc,"--solver",s.msc,"--solver-time-limit","1"]): + [s.args.minizinc,"--solver",s.msc,"--solver-time-limit","1"], + [s.args.minizinc,"--solver",s.msc,"--native-mode","race","--native-race-seconds","5","--solver-time-limit","1"], + [s.args.minizinc,"--solver",s.msc,"--native-mode","configured","--native-branching","reliability","--native-neighborhood","hamming","--solver-time-limit","1"]): code, stdout, stderr = s.run("actual-timeout",[*prefix,large]) require(code == 0 and "=====UNKNOWN=====" in stdout and "=====ERROR=====" not in stdout, f"Timeout became solver error: {code} {stdout!r} {stderr!r}") +def native_controls(s): + # Independent original-model oracle, including all optimal ties. No native + # result or flattened model is used to calculate this answer. + weights, profits = (3,3,2,2,4,1), (5,4,3,3,6,1) + feasible = {x+(sum(p*v for p,v in zip(profits,x)),) for x in itertools.product((0,1), repeat=6) + if sum(w*v for w,v in zip(weights,x)) <= 8 and 3*x[0]+3*x[1] <= 5 and sum(x[2:5]) <= 2} + optimum = max(x[-1] for x in feasible) + optimal = {x for x in feasible if x[-1] == optimum} + source = s.fixture("native-controls") + s.positive("native-controls", optimal, required="bool2int") + + def invoke(label, mode="auto", *flags, source=source): + return s.mzn("native-"+label, "--native-mode", mode, "--native-diagnostics", "on", *flags, source) + + def completed(label, mode="auto", *flags, source=source, allowed=optimal, configuration=(), backend=None, policy=None): + code, stdout, stderr = invoke(label, mode, *flags, source=source) + require(code == 0 and not stderr, f"Native {label}: {code} {stdout!r} {stderr!r}") + lines = [line for line in stdout.splitlines() if line and not line.startswith("%")] + require(len(lines) == 3 and lines[1:] == ["----------", "=========="], f"Native markers {label}: {lines}") + require(tuple(json.loads(lines[0])) in allowed, f"Original oracle failed for {label}: {lines[0]}") + require("% guarantee: exact integer search" in stdout and f"% native-mode: {mode}" in stdout, + f"Native route provenance absent for {label}: {stdout}") + config = next((line for line in stdout.splitlines() if line.startswith("% native-configuration: ")), "") + require(config and all(item in config.split() for item in configuration), f"Settings not forwarded for {label}: {config}") + if backend: + require(f"% native-backend: {backend}" in stdout, f"Wrong actual backend for {label}: {stdout}") + if policy: + require(any(policy in line for line in stdout.splitlines() if line.startswith("% native-policy: ")), + f"Wrong actual policy for {label}: {stdout}") + work = next((line for line in stdout.splitlines() if line.startswith("% native-work: ")), "") + counters = {key:int(value) for key,value in re.findall(r"([a-z-]+)=(\d+)", work)} + s.native_results.append({"case": label, "mode": mode, "solution": json.loads(lines[0]), + "configuration": config[len("% native-configuration: "):], "work": counters, + "policy": next(line[len("% native-policy: "):] for line in stdout.splitlines() if line.startswith("% native-policy: ")), + "backend": next(line[len("% native-backend: "):] for line in stdout.splitlines() if line.startswith("% native-backend: "))}) + return counters, stdout + + completed("auto") + knapsack_points = {x+(sum(p*v for p,v in zip(profits,x)),) for x in itertools.product((0,1), repeat=6) + if sum(w*v for w,v in zip(weights,x)) <= 8} + knapsack_best = max(x[-1] for x in knapsack_points) + knapsack_optimal = {x for x in knapsack_points if x[-1] == knapsack_best} + knapsack = s.fixture("native-knapsack") + completed("knapsack-auto", source=knapsack, allowed=knapsack_optimal, policy="eligible exact knapsack DP") + _, stdout = completed("knapsack-disabled", "auto", "--native-auto-knapsack", "off", source=knapsack, + allowed=knapsack_optimal, configuration=("auto-knapsack=off",)) + require("eligible exact knapsack DP" not in stdout, "Disabled knapsack DP was still selected") + for name in ("presolve", "components", "symmetry", "knapsack"): + completed("auto-no-"+name, "auto", "--native-auto-"+name, "off", configuration=("auto-"+name+"=off",)) + disabled = [item for name in ("presolve", "components", "symmetry", "knapsack") + for item in ("--native-auto-"+name, "off")] + completed("auto-all-disabled", "auto", *disabled, configuration=tuple("auto-"+name+"=off" for name in ("presolve", "components", "symmetry", "knapsack"))) + completed("plain", "plain", backend="Gecode native", configuration=("ordinary-native",)) + completed("uint64-limit", "plain", "--native-node-limit", "18446744073709551615", configuration=("node-limit=18446744073709551615",)) + completed("race", "race", "--native-race-seconds", "0.05", "--native-race-nodes", "4", + configuration=("race-seconds=0.05", "race-nodes=4"), policy="Native sequential race:") + completed("race-zero", "race", "--native-race-seconds", "0", configuration=("race-seconds=0",), policy="skipped") + completed("race-global", "race", source=s.fixture("all-different"), allowed={(1,2)}, policy="skipped") + for order in ("bab", "dfs", "best-bound"): + completed("search-"+order, "configured", "--native-search", order, + configuration=("search="+order,), backend="Gecode native" if order == "bab" else "Gecode native frontier") + work, _ = completed("reliability", "configured", "--native-branching", "reliability", + "--native-branching-probes", "32", "--native-max-open-nodes", "128", + configuration=("branching=reliability", "branching-probes=32", "max-open-nodes=128")) + require(0 < work.get("branching-probes",0) <= 32, "Reliability accepted without executing its probes") + work, _ = completed("reliability-zero", "configured", "--native-branching", "reliability", "--native-branching-probes", "0") + require(work.get("branching-probes") == 0, "Zero reliability probe cap ignored") + work, _ = completed("hamming", "configured", "--native-neighborhood", "hamming", "--native-neighborhood-radius", "1", + "--native-neighborhood-nodes", "32", "--native-neighborhood-seconds", "0.1", + configuration=("neighborhood=hamming", "neighborhood-radius=1", "neighborhood-nodes=32", "neighborhood-seconds=0.1")) + require(work.get("neighborhood-attempts",0) > 0, "Hamming accepted without executing an attempt") + for cap in ("nodes", "seconds"): + work, _ = completed("hamming-zero-"+cap, "configured", "--native-neighborhood", "hamming", "--native-neighborhood-"+cap, "0") + require(work.get("neighborhood-attempts") == 0, "Zero neighborhood cap ignored") + completed("combined-search", "configured", "--native-search", "best-bound", "--native-branching", "reliability", "--native-neighborhood", "hamming") + + # This gate also runs in native-only builds. Discover unavailable checked LP + # through its explicit rejection, never through a successful silent fallback. + code, stdout, stderr = invoke("lp-capability", "configured", "--native-search", "bab", "--native-lp", "root") + checked_lp = code == 0 + if not checked_lp: + require(code != 0 and "checked LP requires HiGHS" in stderr and "----------" not in stdout, + f"Unexpected checked LP failure: {code} {stdout!r} {stderr!r}") + lp_cases = [ + ("lp-root", ("--native-search", "bab", "--native-lp", "root")), + ("lp-root-covers", ("--native-lp", "root", "--native-root-cuts", "on")), + ("lp-updated", ("--native-search", "best-bound", "--native-lp", "updated", "--native-lp-interval", "2", "--native-bound-tightening", "off")), + ("lp-combined", ("--native-lp", "updated", "--native-root-cuts", "on", "--native-branching", "reliability", "--native-neighborhood", "hamming")), + ] + for label, flags in lp_cases: + if checked_lp: + work, stdout = completed(label, "configured", *flags, + configuration=tuple(flags[i][len("--native-"):]+"="+flags[i+1] for i in range(0,len(flags),2))) + if label in ("lp-root-covers", "lp-combined"): + require(work.get("root-cuts",0) > 0, f"Root covers enabled without generating a verified cut: {label}") + require(work.get("lp-calls",0) > 0 and work.get("checked-bounds",0) > 0, + f"Checked LP accepted without checked deductions: {label} {stdout}") + else: + code, stdout, stderr = invoke(label, "configured", *flags) + require(code != 0 and "checked LP requires HiGHS" in stderr and "----------" not in stdout, + f"Explicit LP silently fell back: {label}") + + # Shared finite budgets must never publish a false witness or completion. + # Both the optional algorithms and the ordinary frontier consume this cap. + for mode in ("auto", "race", "plain", "configured"): + for cap in ("0", "1"): + flags = ["--native-node-limit", cap] + if mode == "configured": + flags += ["--native-branching", "reliability", "--native-neighborhood", "hamming"] + code, stdout, stderr = invoke("node-"+mode+"-"+cap, mode, *flags) + require(code == 0 and "=====ERROR=====" not in stdout and "=====UNSATISFIABLE=====" not in stdout, + f"Node cap became error/false infeasibility: {mode} {cap} {stdout!r} {stderr!r}") + lines = [line for line in stdout.splitlines() if line and not line.startswith("%")] + if lines and lines[0].startswith("["): + witness = tuple(json.loads(lines[0])) + require(witness in feasible, "Limited run published invalid original-model witness") + require("==========" not in lines or witness in optimal, "Limited run claimed false optimum") + else: + require(lines == ["=====UNKNOWN====="], f"Limited run protocol: {lines}") + if mode == "configured": + work_line = next((line for line in stdout.splitlines() if line.startswith("% native-work: ")), "") + work = {key:int(value) for key,value in re.findall(r"([a-z-]+)=(\d+)", work_line)} + require("budget-nodes" in work and work["budget-nodes"] <= int(cap), f"Shared node cap exceeded: {work}") + require(work["budget-nodes"] == work.get("frontier-admitted",0)+work.get("branching-probes",0)+work.get("neighborhood-status-attempts",0), + f"Frontier/probe/neighborhood accounting mismatch: {work}") + if cap == "0": + require("==========" not in lines, "Zero node budget incorrectly completed nontrivial model") + code, stdout, stderr = invoke("zero-open-spaces", "configured", "--native-max-open-nodes", "0") + require(code == 0 and "=====UNKNOWN=====" in stdout and "----------" not in stdout and "==========" not in stdout, + "Zero frontier space cap ignored or became a solver error") + + # Rejected controls must not be ignored by MiniZinc or the driver. Test both + # malformed values and meaningful but incompatible combinations. + rejected = [ + ("--native-mode", "bad"), ("--native-diagnostics", "yes"), + ("--native-node-limit", "-1"), ("--native-node-limit", "18446744073709551616"), + ("--native-mode", "race", "--native-race-seconds", "nan"), + ("--native-mode", "race", "--native-race-nodes", "0"), + ("--native-mode", "plain", "--native-auto-presolve", "off"), + ("--native-race-seconds", "0.1"), ("--native-lp", "root"), + ("--native-mode", "configured", "--native-root-cuts", "on"), + ("--native-mode", "configured", "--native-bound-tightening", "off"), + ("--native-mode", "configured", "--native-lp", "root", "--native-lp-interval", "2"), + ("--native-mode", "configured", "--native-lp", "updated", "--native-lp-interval", "0"), + ("--native-mode", "configured", "--native-search", "bab", "--native-branching", "reliability"), + ("--native-mode", "configured", "--native-search", "bab", "--native-max-open-nodes", "1"), + ("--native-mode", "configured", "--native-search", "bab", "--native-neighborhood", "hamming"), + ("--native-mode", "configured", "--native-branching-probes", "0"), + ("--native-mode", "configured", "--native-neighborhood-radius", "1"), + ("--native-mode", "configured", "--native-neighborhood-nodes", "0"), + ("--native-mode", "configured", "--native-neighborhood-seconds", "0"), + ("--native-mode", "configured", "--native-neighborhood", "hamming", "--native-neighborhood-seconds", "-1"), + ("--native-mode", "configured", "--native-search", "bfs"), + ] + for i, flags in enumerate(rejected): + code, stdout, stderr = s.mzn("native-reject-"+str(i), *flags, source) + require(code != 0 and stderr and "----------" not in stdout and "==========" not in stdout and "=====UNSATISFIABLE=====" not in stdout, + f"Invalid controls accepted or emitted proof: {flags} {code} {stdout!r} {stderr!r}") + + def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("--minizinc", type=Path, required=True) @@ -286,7 +457,7 @@ def main(): "configuration_provided":args.registration is not None, "library_files_sha256":suite.library_hashes, "library_sha256":hashlib.sha256(json.dumps(suite.library_hashes,sort_keys=True,separators=(",",":")).encode()).hexdigest(), - "source_sha256":suite.sources} + "source_sha256":suite.sources,"native_controls":suite.native_results} print(json.dumps(report,sort_keys=True)) finally: suite.close() diff --git a/test/optimize/native_auto.cpp b/test/optimize/native_auto.cpp index 2702171a7d..13f3ccbbee 100644 --- a/test/optimize/native_auto.cpp +++ b/test/optimize/native_auto.cpp @@ -35,6 +35,9 @@ std::pair> oracle(const ModelSnapshot& m) { std::vector point(m.variables.size()); for(unsigned i=0;i>i)&1U; bool valid=true; + for(const auto& variable:m.variables) + valid=valid && point[variable.variable.id]>=variable.lower && + point[variable.variable.id]<=variable.upper; for(const auto& row:m.rows)if(row.active){ double value=0;for(auto t:row.terms)value+=t.coefficient*point[t.variable.id]; valid=valid && value>=row.lower && value<=row.upper; @@ -57,9 +60,85 @@ void check(const ModelSnapshot& s,const SolveResult& r,double optimum){ double value=s.objective.offset; for(auto t:s.objective.terms)value+=t.coefficient*r.values[t.variable.id]; assert(value==optimum); - for(const auto& v:s.variables)assert(r.values[v.variable.id]==0 || r.values[v.variable.id]==1); + for(const auto& v:s.variables){ + assert(r.values[v.variable.id]==0 || r.values[v.variable.id]==1); + assert(r.values[v.variable.id]>=v.lower && r.values[v.variable.id]<=v.upper); + } for(const auto& row:s.rows){double a=0;for(auto t:row.terms)a+=t.coefficient*r.values[t.variable.id];assert(a>=row.lower && a<=row.upper);} } + +void configuration(const SolveOptions& solve,bool lp) { + NativeAutoOptions options;options.solve=solve; + // Isolate the transformations so a disabled feature cannot be masked by a + // different coordinator solving the fixture first. + for(int feature=0;feature<3;++feature){ + Model m;std::vector x;std::vector sum,cost; + for(int i=0;i<6;++i){ + x.push_back(feature==0 && i==0 ? m.add_variable(VariableType::Binary,1,1):m.add_binary()); + sum.push_back({x.back(),1});cost.push_back({x.back(),feature==2?1.0:double(i+1)}); + } + if(feature==1){ + m.add_row({{x[0],1},{x[1],1},{x[2],1}},1,2); + m.add_row({{x[3],1},{x[4],1},{x[5],1}},1,2); + } else m.add_row(sum,2,4); + m.minimize(cost,-9); + const auto source=m.snapshot();const auto expected=oracle(source).first; + const char* markers[]={"Exact integer presolve (","independent components","duplicate-column symmetry"}; + for(bool enabled:{false,true}){ + options.settings={false,false,false,false}; + if(feature==0)options.settings.presolve=enabled; + if(feature==1)options.settings.components=enabled; + if(feature==2)options.settings.symmetry=enabled; + const auto result=solve_native_auto_configured(source,options); + check(source,result,expected); + assert((result.message.find(markers[feature])!=std::string::npos)==enabled); + } + } + auto knapsack=fixture(3);const auto source=knapsack.snapshot(); + const auto expected=oracle(source).first; + options.settings={false,false,false,true}; + const auto enabled=solve_native_auto_configured(knapsack,options);check(source,enabled,expected); + options.settings.knapsack=false; + const auto disabled=solve_native_auto_configured(source,options);check(source,disabled,expected); + // Turning off DP must also remove its selection priority: checked LP and + // reliability become available for this eligible weighted binary knapsack. + if(lp){ + assert(enabled.backend=="Gecode native"); + assert(enabled.message.find("eligible exact knapsack DP")!=std::string::npos); + assert(disabled.backend.find("checked LP")!=std::string::npos); + assert(disabled.message.find("eligible exact knapsack DP")==std::string::npos); + } + // A fixed column makes presolve produce a DP-eligible reduced model. Keep + // components disabled so the selected reduced leaf remains observable. + auto reduced=fixture(3);const auto fixed=reduced.add_variable(VariableType::Binary,1,1); + auto cost=reduced.snapshot().objective.terms;cost.push_back({fixed,13});reduced.maximize(cost,-7); + const auto reduced_source=reduced.snapshot(); + options.settings={true,false,true,false}; + const auto reduced_result=solve_native_auto_configured(reduced,options); + check(reduced_source,reduced_result,oracle(reduced_source).first); + assert(reduced_result.message.find("Exact integer presolve (")!=std::string::npos); + if(lp)assert(reduced_result.backend.find("checked LP")!=std::string::npos); + + // All combinations keep the same original feasible set/objective, including + // a disconnected model whose component leaves are eligible for knapsack DP. + Model split;std::vector split_cost; + for(int group=0;group<2;++group){std::vector row; + for(int i=0;i<5;++i){const auto x=split.add_binary();row.push_back({x,double(i+1)}); + split_cost.push_back({x,double(i*3+group+1)});} + split.add_row(row,-inf,7); + } + split.maximize(split_cost,11);const auto split_source=split.snapshot(); + const auto split_expected=oracle(split_source).first; + for(unsigned mask=0;mask<16;++mask){ + options.settings={bool(mask&1),bool(mask&2),bool(mask&4),bool(mask&8)}; + check(split_source,solve_native_auto_configured(split,options),split_expected); + auto stopped=options;stopped.solve.time_limit_seconds=0; + assert(solve_native_auto_configured(split_source,stopped).termination==Termination::TimeLimit); + stopped=options;stopped.solve.cancellation=std::make_shared(); + stopped.solve.cancellation->cancel(); + assert(solve_native_auto_configured(split_source,stopped).termination==Termination::Cancelled); + } +} } int main(){ SolveOptions o;o.backend=Backend::Native;o.guarantee=Guarantee::Exact; @@ -67,10 +146,16 @@ int main(){ if(!native_capabilities().available){ auto m=fixture(0); assert(solve_native_auto(m,o).termination==Termination::Unsupported); + NativeAutoOptions configured;configured.solve=o;configured.settings={false,false,false,false}; + assert(solve_native_auto_configured(m,configured).termination==Termination::Unsupported); + assert(solve_native_auto_configured(m.snapshot(),configured).termination==Termination::Unsupported); + configured.solve.threads=0; + assert(solve_native_auto_configured(m,configured).termination==Termination::InvalidModel); assert(solve(m,o).termination==Termination::Unsupported); std::cout<<"Automatic native disabled-backend checks passed\n";return 0; } const bool lp=native_lp_capabilities().available; + configuration(o,lp); for(int kind=0;kind<5;++kind){ auto m=fixture(kind);auto s=m.snapshot();auto expected=oracle(s); for(bool snapshot:{false,true}){ diff --git a/test/optimize/native_presolve.cpp b/test/optimize/native_presolve.cpp index e9819130b1..a85dffeb5d 100644 --- a/test/optimize/native_presolve.cpp +++ b/test/optimize/native_presolve.cpp @@ -65,6 +65,96 @@ Model reduced_fixture(bool maximum=false) { return model; } +Model auxiliary_fixture(bool maximize,bool bounded,int sign=1) { + Model model;std::vector capacity,equality; + for(int i=0;i<6;++i){const auto x=model.add_binary();capacity.push_back({x,double(i+1)}); + equality.push_back({x,double((maximize?-1:1)*sign*(i*3+1))});} + model.add_row(capacity,-inf,10); + const auto auxiliary=model.add_integer(maximize?3:(bounded?-22:-48),maximize?(bounded?28:54):3); + equality.push_back({auxiliary,double(sign)});model.add_row(equality,3*sign,3*sign); + model.set_objective({{auxiliary,1}},maximize?ObjectiveSense::Maximize:ObjectiveSense::Minimize,-11); + return model; +} + +void objective_auxiliaries() { + SolveOptions options;options.backend=Backend::Native;options.guarantee=Guarantee::Exact; + options.relative_gap=options.absolute_gap=0;options.time_limit_seconds=5; + for(bool maximize:{false,true})for(bool bounded:{false,true})for(int sign:{-1,1}) { + const auto model=auxiliary_fixture(maximize,bounded,sign);const auto source=model.snapshot(); + const auto expected=oracle(source); + for(bool interrupted:{false,true}) { + auto limited=options;limited.node_limit=2;SolveBudget budget(limited);bool called=false; + const auto actual=Detail::native_objective_auxiliary(source,limited,budget, + [&](const ModelSnapshot& reduced,const SolveOptions& exact,SolveBudget& shared) { + called=true;assert(&shared==&budget && exact.guarantee==Guarantee::Exact); + assert(!reduced.variables.back().active && reduced.objective.terms.size()==6); + assert(reduced.rows[1].active==bounded); // Preserve nonredundant auxiliary domain bounds. + auto result=oracle(reduced);shared.add_nodes(2); + if(interrupted){result.termination=Termination::NodeLimit; + result.best_bound=*result.objective+(maximize?3:-3);} + return result; + }); + assert(called && actual && actual->model_id==source.model_id && actual->revision==source.revision); + assert(actual->has_solution() && actual->objective==expected.objective && budget.nodes()==2); + assert(actual->active_variables.back() && actual->values.back()==*actual->objective+11); + assert(validate(source,actual->values,0,0).valid); + assert(actual->termination==(interrupted?Termination::NodeLimit:Termination::Optimal)); + assert(actual->best_bound==*expected.objective+(interrupted?(maximize?3:-3):0)); + } + if(native_capabilities().available)for(bool enabled:{false,true}) { + NativeAutoOptions configured;configured.solve=options;configured.settings={enabled,false,false,true}; + auto actual=solve_native_auto_configured(source,configured); + if(actual.termination!=Termination::Optimal)std::cerr< SolveResult {assert(false);return {};}; + // A second use of the auxiliary or a non-unit equality coefficient must keep + // the original model. No unsupported affine substitution is approximated. + model.add_row({{original.variables.back().variable,1}},3,54); + SolveBudget repeated(options);assert(!Detail::native_objective_auxiliary(model.snapshot(),options,repeated,never)); + auto nonunit=original;for(auto& term:nonunit.rows[1].terms)term.coefficient*=2; + nonunit.rows[1].lower*=2;nonunit.rows[1].upper*=2; + SolveBudget nonunit_budget(options);assert(!Detail::native_objective_auxiliary(nonunit,options,nonunit_budget,never)); + auto started=options;const auto witness=oracle(original); + for(const auto& v:original.variables)started.primal_start.push_back({v.variable,witness.values[v.variable.id]}); + SolveBudget start_budget(started);assert(!Detail::native_objective_auxiliary(original,started,start_budget,never)); + auto cancelled=options;cancelled.cancellation=std::make_shared(); + SolveBudget cancel_budget(cancelled); + const auto stopped=Detail::native_objective_auxiliary(original,cancelled,cancel_budget, + [&](const ModelSnapshot& reduced,const SolveOptions&,SolveBudget&){ + auto result=oracle(reduced);cancelled.cancellation->cancel();return result; + }); + assert(stopped && stopped->termination==Termination::Cancelled && !stopped->has_solution() && !stopped->best_bound); + SolveBudget foreign_budget(options); + const auto foreign=Detail::native_objective_auxiliary(original,options,foreign_budget, + [&](const ModelSnapshot& reduced,const SolveOptions&,SolveBudget&){auto result=oracle(reduced);++result.model_id;return result;}); + assert(foreign && foreign->termination==Termination::BackendError && !foreign->has_solution()); + SolveBudget mask_budget(options); + const auto mask=Detail::native_objective_auxiliary(original,options,mask_budget, + [&](const ModelSnapshot& reduced,const SolveOptions&,SolveBudget&){ + auto result=oracle(reduced);result.active_variables[0]=false;return result; + }); + assert(mask && mask->termination==Termination::BackendError && !mask->has_solution()); + SolveBudget unsupported_budget(options); + const auto unsupported=Detail::native_objective_auxiliary(original,options,unsupported_budget, + [&](const ModelSnapshot& reduced,const SolveOptions&,SolveBudget&){ + SolveResult result;result.model_id=reduced.model_id;result.revision=reduced.revision; + result.guarantee=Guarantee::Exact;result.termination=Termination::Unsupported;return result; + }); + assert(!unsupported); // The caller retains the originally admitted native route. +} + void fixed_offsets_and_bounds() { for (bool maximum:{false,true}) for (auto guarantee:{Guarantee::Exact,Guarantee::Numerical}) { const auto model=reduced_fixture(maximum); const auto source=model.snapshot(); @@ -171,6 +261,6 @@ void starts_and_stops() { } int main() { - fixed_offsets_and_bounds(); infeasibility_and_fixpoint(); incomplete_artifact(); starts_and_stops(); + objective_auxiliaries(); fixed_offsets_and_bounds(); infeasibility_and_fixpoint(); incomplete_artifact(); starts_and_stops(); std::cout<<"Exact native presolve composition: offsets, proof transfer, partial reductions, starts and stops pass\n"; } diff --git a/test/optimize/native_race.cpp b/test/optimize/native_race.cpp index 0955224b13..a19a46cf01 100644 --- a/test/optimize/native_race.cpp +++ b/test/optimize/native_race.cpp @@ -51,7 +51,10 @@ int main(){ o.solve.relative_gap=o.solve.absolute_gap=0;o.solve.time_limit_seconds=5; o.exploration_seconds=1;o.probe_node_limit=1; if(!native_capabilities().available){auto m=fixture(false,0); - assert(solve_native_race(m,o).termination==Termination::Unsupported);return 0;} + o.automatic={false,false,false,false}; + assert(solve_native_race(m,o).termination==Termination::Unsupported); + o.probe_node_limit=0; + assert(solve_native_race(m,o).termination==Termination::InvalidModel);return 0;} bool saw_two=false; for(bool maximize:{false,true})for(int seed=0;seed<4;++seed){ auto m=fixture(maximize,seed);auto s=m.snapshot();auto optimum=oracle(s); @@ -68,6 +71,16 @@ int main(){ } auto disabled=o;disabled.exploration_seconds=0; auto d=solve_native_race(s,disabled);check(s,d,optimum);assert(d.termination==Termination::Optimal); + // Configured automatic candidates retain the same original semantics and + // obey the global cap across both probes and the selected restart. + auto configured=o;configured.automatic={false,false,false,false}; + auto configured_result=solve_native_race(s,configured);check(s,configured_result,optimum); + assert(configured_result.termination==Termination::Optimal); + configured.solve.node_limit=2; + configured_result=solve_native_race(s,configured);check(s,configured_result,optimum); + assert(configured_result.termination==Termination::Optimal || configured_result.termination==Termination::NodeLimit); + const auto nodes=configured_result.message.find("cumulative nodes=");assert(nodes!=std::string::npos); + assert(std::stoull(configured_result.message.substr(nodes+17))<=2); auto start=o;for(auto v:s.variables)start.solve.primal_start.push_back({v.variable,result.values[v.variable.id]}); auto started=solve_native_race(s,start);check(s,started,optimum); assert(started.message.find("Native race skipped")==0); @@ -77,6 +90,18 @@ int main(){ assert(solve_native_race(s,stopped).termination==Termination::Cancelled); } assert(saw_two); + // Disabled exploration still forwards settings, rather than falling back to + // an unconfigured automatic solve. Isolate symmetry to observe its effect. + Model symmetric;std::vector terms; + for(int i=0;i<6;++i)terms.push_back({symmetric.add_binary(),1}); + symmetric.add_row(terms,2,4);symmetric.minimize(terms,-3); + for(bool enabled:{false,true}){ + auto configured=o;configured.exploration_seconds=0; + configured.automatic={false,false,enabled,false}; + auto result=solve_native_race(symmetric,configured);check(symmetric.snapshot(),result,-1); + assert(result.termination==Termination::Optimal && result.message.find("Native race skipped")==0); + assert((result.message.find("duplicate-column symmetry")!=std::string::npos)==enabled); + } auto m=fixture(false,0);auto invalid=o;invalid.exploration_seconds=-1; assert(solve_native_race(m,invalid).termination==Termination::InvalidModel); invalid=o;invalid.probe_node_limit=0; diff --git a/tools/flatzinc/fzn-gecode-optimize.cpp b/tools/flatzinc/fzn-gecode-optimize.cpp index c035023f83..23b8a6ecc5 100644 --- a/tools/flatzinc/fzn-gecode-optimize.cpp +++ b/tools/flatzinc/fzn-gecode-optimize.cpp @@ -2,6 +2,7 @@ #include #include #include +#include #include #include #include @@ -23,6 +24,14 @@ struct Options { bool minizinc=false; F::Options capture; O::SolveOptions solve; + std::string native_mode="auto",lp="off",search="dfs",branching="default",neighborhood="off"; + O::NativeAutoSettings automatic; + O::NativeRaceOptions race; + O::NativeLpSettings relaxation; + O::NativeBranchingSettings branching_settings; + O::NativeNeighborhoodSettings neighborhood_settings; + std::size_t max_open_nodes=100000; + bool root_cuts=false,diagnostics=false; Options() { solve.backend=O::Backend::Native;solve.guarantee=O::Guarantee::Exact; solve.relative_gap=0;solve.absolute_gap=0; @@ -33,7 +42,20 @@ const char* usage() { "[--time-limit SECONDS] [--node-limit N] [--max-input-bytes N]\n" "One satisfaction solution or final optimization; bounded integer/Boolean subset.\n" "Native uses exact integer search; HiGHS is explicitly numerical.\n" - "MiniZinc protocol: --minizinc [-t MILLISECONDS] MODEL.fzn|-\n"; + "MiniZinc protocol: --minizinc [-t MILLISECONDS] [NATIVE OPTIONS] MODEL.fzn|-\n" + "Native options (all take a value):\n" + " --native-mode auto|race|plain|configured (default auto)\n" + " --native-auto-presolve/--native-auto-components/--native-auto-symmetry/--native-auto-knapsack on|off\n" + " --native-race-seconds SECONDS --native-race-nodes N (race only)\n" + " --native-lp off|root|updated --native-root-cuts on|off\n" + " --native-bound-tightening on|off --native-lp-interval N\n" + " --native-search bab|dfs|best-bound --native-max-open-nodes N\n" + " --native-branching default|reliability --native-branching-probes N\n" + " --native-neighborhood off|hamming --native-neighborhood-radius N\n" + " --native-neighborhood-nodes N --native-neighborhood-seconds SECONDS\n" + " LP/search/neighborhood controls require configured mode.\n" + " --native-node-limit N --native-diagnostics on|off\n" + "Racing uses sequential probes and restarts: it can increase total CPU and solve time.\n"; } std::uint64_t count(const std::string& text) { if(text.empty())throw std::invalid_argument("Empty count"); @@ -52,9 +74,93 @@ double seconds(const std::string& text) { throw std::invalid_argument("Time limit must be finite and nonnegative"); return value; } +bool on_off(const std::string& value) { + if(value=="on")return true;if(value=="off")return false; + throw std::invalid_argument("Boolean native options must be on or off"); +} +std::size_t size_count(const std::string& value) { + const auto n=count(value); + if(n>std::numeric_limits::max())throw std::invalid_argument("Count exceeds size_t range"); + return static_cast(n); +} +std::string choice(const std::string& key,const std::string& value,std::initializer_list choices) { + for(const auto* accepted:choices)if(value==accepted)return value; + throw std::invalid_argument("Invalid value for "+key+": "+value); +} +bool native_argument(Options& o,const std::string& key,const std::string& value) { + if(key=="--native-mode")o.native_mode=choice(key,value,{"auto","race","plain","configured"}); + else if(key=="--native-auto-presolve")o.automatic.presolve=on_off(value); + else if(key=="--native-auto-components")o.automatic.components=on_off(value); + else if(key=="--native-auto-symmetry")o.automatic.symmetry=on_off(value); + else if(key=="--native-auto-knapsack")o.automatic.knapsack=on_off(value); + else if(key=="--native-race-seconds")o.race.exploration_seconds=seconds(value); + else if(key=="--native-race-nodes") { + o.race.probe_node_limit=count(value); + if(!o.race.probe_node_limit)throw std::invalid_argument("Native race node budget must be positive"); + } else if(key=="--native-lp")o.lp=choice(key,value,{"off","root","updated"}); + else if(key=="--native-root-cuts")o.root_cuts=on_off(value); + else if(key=="--native-bound-tightening")o.relaxation.bound_tightening=on_off(value); + else if(key=="--native-lp-interval") { + const auto n=count(value); + if(!n||n>std::numeric_limits::max())throw std::invalid_argument("LP interval must be a positive unsigned integer in range"); + o.relaxation.bound_change_interval=static_cast(n); + } else if(key=="--native-search")o.search=choice(key,value,{"bab","dfs","best-bound"}); + else if(key=="--native-branching")o.branching=choice(key,value,{"default","reliability"}); + else if(key=="--native-branching-probes")o.branching_settings.max_probe_status_calls=count(value); + else if(key=="--native-max-open-nodes")o.max_open_nodes=size_count(value); + else if(key=="--native-neighborhood")o.neighborhood=choice(key,value,{"off","hamming"}); + else if(key=="--native-neighborhood-radius")o.neighborhood_settings.radius=size_count(value); + else if(key=="--native-neighborhood-nodes")o.neighborhood_settings.max_status_calls=count(value); + else if(key=="--native-neighborhood-seconds")o.neighborhood_settings.time_limit_seconds=seconds(value); + else if(key=="--native-node-limit")o.solve.node_limit=count(value); + else if(key=="--native-diagnostics")o.diagnostics=on_off(value); + else return false; + return true; +} +O::NativeSearchOptions search_options(const Options& o,const O::SolveOptions& solve) { + O::NativeSearchOptions result;result.solve=solve; + result.order=o.search=="best-bound"?O::NativeSearchOrder::BestBound:O::NativeSearchOrder::DepthFirst; + result.max_open_nodes=o.max_open_nodes; + if(o.lp!="off")result.relaxation=o.relaxation; + if(o.branching=="reliability")result.branching=o.branching_settings; + return result; +} +void validate_arguments(Options& o,const std::set& seen) { + for(const auto& key:seen) { + if(key.compare(0,9,"--native-")!=0)continue; + if(o.solve.backend!=O::Backend::Native)throw std::invalid_argument("Native controls require the native backend"); + if(key=="--native-mode"||key=="--native-node-limit"||key=="--native-diagnostics")continue; + if(key.compare(0,14,"--native-auto-")==0) { + if(o.native_mode!="auto"&&o.native_mode!="race")throw std::invalid_argument(key+" requires auto or race mode"); + } else if(key.compare(0,14,"--native-race-")==0) { + if(o.native_mode!="race")throw std::invalid_argument(key+" requires race mode"); + } else if(o.native_mode!="configured")throw std::invalid_argument(key+" requires configured mode"); + } + const auto requires=[&](const std::string& key,bool valid,const std::string& reason) { + if(seen.count(key)&&!valid)throw std::invalid_argument(key+" requires "+reason); + }; + requires("--native-root-cuts",o.lp!="off","LP enabled"); + requires("--native-bound-tightening",o.lp!="off","LP enabled"); + requires("--native-lp-interval",o.lp=="updated","updated LP frequency"); + requires("--native-branching",o.search!="bab","frontier search (dfs or best-bound)"); + requires("--native-max-open-nodes",o.search!="bab","frontier search (dfs or best-bound)"); + requires("--native-neighborhood",o.search!="bab","frontier search (dfs or best-bound)"); + requires("--native-branching-probes",o.branching=="reliability","reliability branching"); + for(const auto* key:{"--native-neighborhood-radius","--native-neighborhood-nodes","--native-neighborhood-seconds"}) + requires(key,o.neighborhood=="hamming","Hamming neighborhoods"); + o.relaxation.frequency=o.lp=="updated"?O::NativeLpFrequency::AfterBoundChanges:O::NativeLpFrequency::Root; + if(o.root_cuts)o.relaxation.root_cover_cuts=O::NativeRootCoverSettings{}; + o.solve.validate(); + if(o.native_mode=="race") {o.race.solve=o.solve;o.race.automatic=o.automatic;o.race.validate();} + if(o.native_mode=="configured") { + if(o.lp!="off")o.relaxation.validate(); + if(o.search!="bab")search_options(o,o.solve).validate(); + if(o.neighborhood=="hamming")o.neighborhood_settings.validate(); + } +} Options arguments(const std::vector& args) { if(!args.empty()&&args[0]=="--minizinc") { - Options options;options.minizinc=true;bool timed=false,filename_only=false; + Options options;options.minizinc=true;bool timed=false,filename_only=false;std::set seen; for(std::size_t i=1;i& args) { timed=true;const auto milliseconds=count(args[++i]); // MiniZinc 2.10.1 treats a zero solver time limit as unlimited. if(milliseconds)options.solve.time_limit_seconds=static_cast(milliseconds)/1000.0; + } else if(!filename_only&&arg.compare(0,9,"--native-")==0) { + if(i+1==args.size()||!seen.insert(arg).second)throw std::invalid_argument("Missing or repeated option: "+arg); + if(!native_argument(options,arg,args[++i]))throw std::invalid_argument("Unsupported MiniZinc protocol option: "+arg); } else if(arg.empty()||(!filename_only&&arg[0]=='-'&&arg!="-")) throw std::invalid_argument("Unsupported MiniZinc protocol option: "+arg); else { @@ -71,14 +180,15 @@ Options arguments(const std::vector& args) { } } if(options.filename.empty())throw std::invalid_argument("MiniZinc protocol requires exactly one model"); - options.capture.source=options.filename;options.solve.validate();return options; + options.capture.source=options.filename;validate_arguments(options,seen);return options; } if(args.empty()||args[0].empty()||(args[0][0]=='-'&&args[0]!="-")) throw std::invalid_argument(usage()); Options options;options.filename=args[0];options.capture.source=args[0];std::set seen; for(std::size_t i=1;i& args) { const auto n=count(value); if(n>static_cast(std::numeric_limits::max()))throw std::invalid_argument("Input limit exceeds parser index range"); options.capture.max_input_bytes=static_cast(n); - } else throw std::invalid_argument("Unsupported option: "+key); + } else if(!native_argument(options,key,value))throw std::invalid_argument("Unsupported option: "+key); } - options.solve.validate();return options; + // The historical unprefixed node limit is also valid with HiGHS. + if(seen.count("--native-node-limit")&&std::find(args.begin(),args.end(),"--native-node-limit")==args.end())seen.erase("--native-node-limit"); + validate_arguments(options,seen);return options; +} +struct SolveOutput {O::SolveResult result;std::string work;}; +std::string lp_work(const O::NativeLpStatistics& s) { + return "lp-calls="+std::to_string(s.lp_calls)+" checked-bounds="+std::to_string(s.valid_bounds)+ + " root-cuts="+std::to_string(s.root_cover.cuts)+" variable-fixings="+std::to_string(s.variable_fixings)+ + " bound-tightenings="+std::to_string(s.variable_bound_tightenings); +} +SolveOutput search_output(O::NativeSearchResult result) { + auto work=lp_work(result.relaxation)+" frontier-admitted="+std::to_string(result.frontier.admitted_nodes)+ + " branching-probes="+std::to_string(result.branching.probe_status_calls)+ + " budget-nodes="+std::to_string(result.branching.budget_nodes); + return {std::move(result.result),std::move(work)}; +} +const char* neighborhood_completion(O::NativeNeighborhoodCompletion value) { + using C=O::NativeNeighborhoodCompletion; + switch(value) { + case C::NotStarted:return "not-started"; + case C::NoIncumbent:return "no-incumbent"; + case C::ProofCompletedBeforeAttempt:return "proof-completed-before-attempt"; + case C::NoEligibleBinary:return "no-eligible-binary"; + case C::NonrestrictingRadius:return "nonrestricting-radius"; + case C::FormulationLimit:return "formulation-limit"; + case C::SourceLimit:return "source-limit"; + case C::WorkLimit:return "work-limit"; + case C::StatusLimit:return "status-limit"; + case C::SharedNodeReserve:return "shared-node-reserve"; + case C::LocalStorageLimit:return "local-storage-limit"; + case C::LocalTimeLimit:return "local-time-limit"; + case C::NoImprovement:return "no-improvement"; + case C::Improved:return "improved"; + case C::GlobalStop:return "global-stop"; + case C::Error:return "error"; + } + return "unknown"; +} +SolveOutput dispatch(const O::ModelSnapshot& model,const Options& o,const O::SolveOptions& solve) { + if(solve.backend!=O::Backend::Native)return {O::solve(model,solve),{}}; + if(o.native_mode=="plain")return {O::solve_native(model,solve),{}}; + if(o.native_mode=="auto") { + O::NativeAutoOptions automatic;automatic.solve=solve;automatic.settings=o.automatic; + return {O::solve_native_auto_configured(model,automatic),{}}; + } + if(o.native_mode=="race") { + auto race=o.race;race.solve=solve;race.automatic=o.automatic; + return {O::solve_native_race(model,race),{}}; + } + if(o.search=="bab") { + if(o.lp=="off")return {O::solve_native(model,solve),{}}; + O::NativeLpOptions lp;static_cast(lp)=o.relaxation;lp.solve=solve; + auto result=O::solve_native_lp(model,lp);auto work=lp_work(result.relaxation); + return {std::move(result.result),std::move(work)}; + } + auto search=search_options(o,solve); + if(o.neighborhood=="off")return search_output(O::solve_native_search(model,search)); + O::NativeNeighborhoodOptions neighborhood;neighborhood.search=search;neighborhood.neighborhood=o.neighborhood_settings; + auto result=O::solve_native_neighborhoods(model,neighborhood);auto output=search_output(std::move(result.search)); + output.work+=" neighborhood-attempts="+std::to_string(result.neighborhood.attempts)+ + " neighborhood-improvements="+std::to_string(result.neighborhood.accepted_improvements)+ + " neighborhood-status-attempts="+std::to_string(result.neighborhood.status_attempts)+ + " neighborhood-eligible="+std::to_string(result.neighborhood.eligible_variables)+ + " neighborhood-completion="+neighborhood_completion(result.neighborhood.completion); + return output; } #ifdef GECODE_FLATZINC_DRIVER_TEST -O::SolveResult test_solve(const O::ModelSnapshot&,const O::SolveOptions&); +SolveOutput test_solve(const O::ModelSnapshot&,const Options&,const O::SolveOptions&); #endif std::string location(const F::Location& at) { return at.source+(at.line?":"+std::to_string(at.line):""); } struct Output {std::string text;int code=1;}; -Output render(const O::CompiledFlatZinc& compiled,const O::SolveResult& result,const Options& options) { +std::string comment_line(std::string value) { + for(auto& c:value)if(static_cast(c)<32||static_cast(c)==127)c=' '; + return value; +} +std::string configuration(const Options& o) { + std::ostringstream text;text.imbue(std::locale::classic()); + const auto on=[](bool value){return value?"on":"off";}; + if(o.native_mode=="auto"||o.native_mode=="race") { + text<<"auto-presolve="<model(),solve_options); + auto solved=test_solve(compiled.compiled->model(),options,solve_options); #else - auto result=O::solve(compiled.compiled->model(),solve_options); + auto solved=dispatch(compiled.compiled->model(),options,solve_options); #endif // The parser has cooperative stage boundaries, not token-level interruption. // Never publish a newly returned point after the overall frontend deadline. if(expired())return unknown(); - auto output=render(*compiled.compiled,result,options); + const auto& result=solved.result; + auto output=render(*compiled.compiled,result,options,solved.work); if(expired())return unknown(); out<