gecode/optimize/native.hpp provides an optional compiler from the sparse optimization model to actual native Gecode Space, IntVarArray, integer propagators and branch-and-bound search. It is an additive route: existing native Gecode modeling, globals, search classes and FlatZinc behavior are not changed. The typed global registry retains six native constraint families. The owning FlatZinc capture/compiler and separate command-line route support a documented subset; broader global and FlatZinc predicate coverage remain future work.
solve_native(ModelSnapshot, options) and solve_native(Model, options) accept backend Auto or Native; explicitly requesting Highs is a mismatch and returns Unsupported. The entry point itself always selects native search. native_capabilities() reports whether this bridge was compiled in and its supported subset. The common dispatcher controls its own Auto policy.
The common solve(model, options) routes Backend::Native here, and capabilities(Backend::Native) exposes the same capability report. Common Auto selects native Gecode for active native globals and HiGHS for other models. The result always identifies the actual backend; explicit selections are never substituted.
Build the bridge from the repository root with GECODE_ENABLE_OPTIMIZE=ON, the integer/search components enabled, and GECODE_OPTIMIZE_WITH_NATIVE=ON. The last option defaults to ON when those native components exist. A standalone -S gecode/optimize build supports the numerical or backend-free component; explicitly requesting native support there fails with top-level build instructions. HiGHS can be disabled in a combined native-only optimization build with GECODE_OPTIMIZE_WITH_HIGHS=OFF. Its explicit native route still works.
Supported mathematical subset
- Every active variable has type Integer, Binary or SemiInteger, with finite integral bounds inside Gecode::Int::Limits::min through max. Semi-integer domains are exactly {0} union [lower, upper], represented by a native IntSet; their zero alternative is retained.
- Original linear coefficients and finite row bounds are integral and inside the same native limits. Infinite row sides are allowed. Equality, lower-only, upper-only, ranged, empty and redundant rows are supported.
- Each original row and each original indicator expression must satisfy sum_i max(abs(a_i*effective_lower_i), abs(a_i*upper_i)) <= Int::Limits::max. Effective lower bounds include zero for semi-integer variables. This conservative condition bounds all products and partial activities without relying on cancellation or on other constraints to tighten domains.
- Both objective senses are supported. The objective expression obeys the same activity condition with Int::Limits::max / 2, reserving space for the native cost equality. The offset is integral, and its magnitude plus the largest absolute attainable expression bound must not exceed 2^53. Thus all objective values can also be represented exactly by the result's double fields.
Unsupported continuous domains, fractional numbers, missing finite variable bounds, and excessive activity/objective ranges return Unsupported before search. Bounds are never silently rounded and an unsupported formulation is never reported as infeasible. Even a fixed continuous variable is outside this initial integer compiler. A caller may construct an explicitly equivalent integer model, but the bridge does not infer or rewrite that intent.
Bounded binary knapsack strengthening
Ordinary native search recognizes one narrow exact subproblem at the root: every active variable must be an original Binary with domain exactly [0,1], and one capacity row must cover every active column with strictly positive integer weights. The row may be written as weights*x <= capacity or its sign-reversed lower-bound form. An opposite side is allowed only when it is nonrestrictive for nonnegative weights. Active indicators, globals, additional rows, uncovered variables, fixed binaries and binary-valued Integer variables use the existing native path.
An exact dynamic program minimizes the signed objective over this capacity row. Maximization negates the coefficients internally; the offset is kept separate. Capacity is capped at 65,536 and the full table, including its base row, at 1,000,000 int64_t entries (at most 8 MB). Larger instances fall back before table allocation. An objective for which all-zero is already optimal also keeps the ordinary minimum-first path. The recurrence uses work proportional to the admitted table size; it is pseudo-polynomial in numeric capacity.
The reconstructed binary witness is checked against the capacity and objective before use. The native space receives only the proven objective-side bound (cost >= optimum for minimization, reversed for maximization), which preserves all original feasible assignments. The owning witness orders native choices; it never fixes the model or directly publishes a result. Ordinary native search, strict incumbent cutoffs and independent original-model candidate checking still establish the returned status and solution.
This work runs once during root construction and shares cancellation and time limits, with checks inside the table and reconstruction loops. It consumes no search-node admissions. Allocation failure follows the existing MemoryLimit contract; time or cancellation does not publish an unfinished artifact. Explicit NativeLP, frontier relaxation and restricted local neighborhoods bypass the DP. No generic objective-sign value ordering or generic DFS traversal change is enabled. Benefits apply to this admitted subproblem, not general CP or MIP.
Original indicators and exact validation
Active typed indicators use their original row and activation value. The compiler validates the entire mutable snapshot, including generated-row origins, captured domains and guarded numerical lowerings, then replaces those generated rows with native reified integer constraints. For a ranged indicator both sides are implications from the same activation literal. The numerical helper's optional inactive gate retains its exact equality with the activator, so objectives and other rows that reference that exposed gate keep their meaning. Nonintegral, outward-rounded M values in the discarded lowering do not make an otherwise supported original integer indicator unsupported.
Every candidate is mapped back to the original variable slots, including tombstones. A separate integer checker reads the original snapshot, checks variable domains, original rows, original indicators and gate equalities, and recomputes the objective using int64_t. Its arithmetic is protected by the compiler's product and absolute-activity limits. The native cost variable must match that recomputed objective. The candidate must additionally pass the existing original-model numerical checker, including its retained numerical lowerings, before solution_validated can become true.
Guarantee::Exact therefore refers to preserved integer arithmetic and native finite-domain search on this explicit subset. It is not just numerical feasibility relabeled as exact. Completed branch-and-bound establishes optimality or infeasibility through native propagation and exhaustive search with sound strict objective cuts. The bridge does not emit an independently checkable proof artifact; Guarantee::Certified returns Unsupported.
Guarantee::Numerical accepts the same supported subset and runs the same integer search and checks. Feasibility and integrality tolerances never relax the integer checker. Relative/absolute gap options do not enable early stopping in this route; it attempts full optimality even when positive gaps are allowed.
Complete native starts
SolveOptions::primal_start accepts one complete exact assignment through solve(..., Backend::Native) and solve_native. Values use owner-aware original variable handles; duplicate, foreign/deleted, nonfinite, nonintegral, out-of-domain or infeasible complete input returns InvalidModel. No rounding is performed, including for a Numerical guarantee or near-integral values. The zero alternative of a SemiInteger domain remains valid.
Supply every active ordinary variable. A missing live indicator inactive_gate is derived from its exact activation relation; chains are completed forward without guessing, and an explicit inconsistent gate is rejected. A retained gate after remove_indicator() has no such live meaning and must be supplied. Other private/fixed slots are not inferred. Any unresolved active slot returns Unsupported; values are never fixed in the original search as partial hints.
Full native preflight and exact original row/indicator/global/objective checks precede publication. A second independent public validator must also pass. A timely accepted start is stored as an owning incumbent (start_submitted and solution_validated true), then the unfixed original root receives a strict integer objective cutoff. Exhausting this improvement problem proves the retained incumbent optimal; it never makes the original model infeasible. Later limits or operational failures preserve an earlier timely validated incumbent, while invalid/late starts publish nothing. The original snapshot, revision, constraints and variable bounds are unchanged.
Start checking uses the shared clock/cancellation token and no search node or extra native propagation. Zero time, pre-cancellation and zero node quota stop before start processing. Model edits require full revalidation and objective recomputation on the next solve; there is no persistent native session or implicit previous-result reuse. This slice does not add repair, partial completion search or an automatic cold-start heuristic. See NATIVE-PRIMALS-DESIGN.md for the later portfolio scope.
Search, limits, and results
The first implementation uses one deterministic worker, smallest-domain-first variable branching and minimum-value-first alternatives. threads != 1, a nonzero random seed, or an unresolved partial primal start returns Unsupported. Complete exact starts are accepted as described above.
One shared SolveBudget covers structural validation, compilation, native search and candidate checking. The Model overload also deducts the time used to create its owning snapshot; moved-from model errors become InvalidModel results instead of escaping that overload. Native search statistics contribute newly visited nodes to the budget. A native stop object checks cancellation, deadline and node limits, in that priority order.
Stopping is cooperative. Individual native propagation and recomputation calls cannot be interrupted, so the wall time may exceed the requested deadline. Budget checks after backend calls and after original-model checking exclude late candidates; an earlier validated incumbent may still be returned. At an exact node-limit boundary the bridge conservatively reports NodeLimit, even if a candidate or exhaustion was observed in the same call.
Interrupted results have no best_bound, absolute gap or relative gap: this bridge does not yet maintain a global bound over the unfinished search frontier. Only proven optimal completion sets best_bound == objective and zero gaps. Proven infeasibility has no incumbent or objective. An exact interrupted incumbent remains an exactly checked feasible witness; its status does not claim optimality. Historical results retain original identity, revision, values and tombstone layout after subsequent model edits.
Build and verification
native.cpp has a backend-disabled stub when GECODE_OPTIMIZE_WITH_NATIVE is absent. Enabling it requires native Gecode integer, search, kernel and support libraries, their matching generated configuration header, and the thread library. It does not require the minimodel library or HiGHS. The build integration owns native dependency discovery and links; the source itself never fetches anything. The native test target must use the same enable macro.
test/optimize/native.cpp compares tiny problems to a separate exhaustive integer oracle for both senses, negative coefficients/offsets, ranged rows, semi-integers and both indicator activation values. It also covers gate references, redundant/constant/empty models, generated fractional M values, model history, tombstones, foreign handles, hostile snapshots, node-limited incumbents, zero deadlines, cancellation, backend mismatch, disabled builds, unresolved partial starts and deliberate integer/floating range failures.
test/optimize/native_starts.cpp independently enumerates the original finite domains and predicates, including globals, semi-integer holes, live and removed gates, and both objective senses. It checks every accepted start against this oracle, then verifies that the original unfixed problem is still optimized. Separate test-hook builds inject cancellation, allocation errors and operational failures around validation, publication, LP preparation, cutoff posting, frontier transfer and cleanup; interrupted bounds are checked against the oracle.
Local complete-start checks passed 2,636 configurations with native Gecode and HiGHS, both normally and with the bridge, test, native libraries and HiGHS built using address/undefined sanitizers. The native-only hook build passed 1,350 configurations. Existing native, LP, frontier, reliability-branching and global regressions also passed. These are correctness checks, not performance benchmarks or a claim of native MILP parity with commercial solvers.
Generated by
1.18.0