Exact linear programming
Solve a bounded standard-form linear program with pure-RiX exact Rational simplex arithmetic.
The fast standard path reports certificateStatus=:notAvailable and points to the exact two-phase option rather than silently omitting evidence.
Equalities, greater-than constraints, and Phase I
The exact solution is (2,1). Phase I introduces and then removes artificial variables; Phase II returns matching primal and dual objective values. This path reports method=:twoPhaseExactSimplex and certificateStatus=:verified.
Free and bounded variables
The free variable is split only inside the canonical model and comes back as -1; the bounded variable is shifted internally and comes back as 3.
Inspect certificates and reuse the final basis
Infeasible results have a negative Phase I optimum. Unbounded results carry a feasible point and exact direction; the checker verifies the direction of every constraint and variable bound, so all nonnegative steps stay feasible, together with strict objective improvement.
Integer coordinates with a resumable queue
Integer axes are one-based coordinate indices. Only those axes are integral; others remain exact Rational coordinates. The FIFO queue branches on the first fractional integer coordinate. Each branch carries inherited relaxation bounds. An exhausted result retains its incumbent, bounds, gap, pending queue and any relaxations whose iteration limit was reached. ResumeMixedInteger extends the node budget after replay; it does not change the per-relaxation iteration budget. For an unresolved relaxation, make a new call with a larger maxIterations. An integer unbounded certificate scales the rational ray to integral increments.
Convex quadratic certificates
The objective is xᵀHx/2 + cᵀx + constant, minimized. Every principal minor checks positive semidefiniteness exactly. Bounded active-set enumeration searches for an exact KKT witness, including primal feasibility, multiplier signs, stationarity and zero active-constraint residuals. A checked witness establishes a global optimum. Nonconvex input returns unsupportedNonconvex; search exhaustion returns unknown. An exact feasibility certificate can prove an empty domain, and an improving feasible ray in the nullspace of H proves unboundedness.
Global boxes and open constraints
Each constraint means expression relation 0, using :le, :lt, :ge, :gt or :eq. This example encloses an infimum of zero while retaining a strictly positive feasible point. boundedGap does not claim that a boundary point is attained. Midpoint samples supply feasible objective bounds; whole-box certified ranges supply global bounds. Strict inequalities are never silently closed. Domain holes, unavailable ranges and depth/evidence limits retain whole unresolved boxes. The method uses no derivative assumptions and reports no local optimum. Opaque callables are unsupported; use an existing calculus expression.
Limits and replay
MILP supports 8 variables and 32 constraints, at most 256 nodes and 4096 simplex iterations per node. Defaults are 64 nodes and 256 iterations. QP supports 6 variables, 16 source constraints and 16 inequalities including variable bounds; defaults are 64 active sets, 4096 masks and 512 iterations (maximums 256, 65536, 4096). Box optimization supports 8 variables, 16 constraints, 256 boxes and depth 32; defaults are 63 boxes, depth 16, objective gap 1/1000 and one range partition. Range partitions are capped at 16. Integer and box queues stop before retained evidence exceeds the shared replay budget and preserve the unprocessed region. Inputs and exact components must fit the shared replay bounds (4096 digits per component). Replay checks are deterministic, bounded and reject altered claims; a successful check validates an exhausted report, not an optimality claim.
solve.System reuses its existing affine compiler: integer=[:x,:y] selects integer outputs; hessian=... selects convex quadratic minimization with the same objective coefficients and domain bounds. Combining these two options is unsupported. Closed affine constraints use the LP path; strict/nonlinear constraints use .solve.OptimizeBox(objective,constraints,box,options) instead. Its result can be replayed by .solve.Check(result). When a Solve result has no proved optimum, its kind is unknown, even if it includes an incumbent.