perf: rebuild presolve as an incremental delta-based bake

klause-cli/src/commonMain/kotlin/com/eignex/klause/cli/CliMode.kt

@@ -5,12 +5,13 @@ import com.eignex.klause.backtrack.lp.LpEmphasis
 import com.eignex.klause.backtrack.lp.LpPlan
 import com.eignex.klause.backtrack.lp.lpHarvestReporting
 import com.eignex.klause.localsearch.DefinitionalSweep
+import com.eignex.klause.presolve.BakeConfig
 import com.eignex.klause.presolve.PresolveConfig
 import com.eignex.klause.presolve.PresolveContext
 import com.eignex.klause.presolve.PresolveEmphasis
 import com.eignex.klause.presolve.PresolvePass
 import com.eignex.klause.presolve.Presolver
-import com.eignex.klause.propagation.PropagationResult
+import com.eignex.klause.presolve.RootBaker
 import com.eignex.klause.solver.Cancellation
 import com.eignex.klause.solver.Problem
 import com.eignex.klause.solver.Sample
@@ -263,7 +264,13 @@ internal fun Solvable.presolved(
     solutionSetSensitive: Boolean,
     cancellation: Cancellation = Cancellation.Never,
 ): Solvable {
+    // Root-bake probing (failed-literal / SAC), formerly baked into the kernel `Problem` at compile
+    // time, now runs in the presolve lane via [RootBaker]: resolve it from the presolve config once and
+    // thread it through the [PresolveContext] so every rebuild re-derives it, and seed the initial
+    // problem up front so the first presolve round sees the same probed root the old self-bake produced.
+    val bakeConfig = BakeConfig.from(config)
     val context = PresolveContext.of(linearObjective, solutionSetSensitive, problem.hasSymmetryBreaking)
+        .withBakeConfig(bakeConfig)
     // LP-relaxation harvest (#10): fold the LP's proven domain tightenings, redundant-row removals and
     // implied equalities into the problem permanently so every backend (local search included) sees them —
     // the backtrack solver's own root shave reaches only its search session. It is a presolve concern, so
@@ -278,14 +285,21 @@ internal fun Solvable.presolved(
     }
     val objective = linearObjective ?: LinearObjective()
 
-    var current = problem
+    val seeded = RootBaker.reseed(problem, bakeConfig)
+    var current = seeded
     val reconstructs = ArrayList<(Sample) -> Sample>() // in application order; round 1 first
     val firedPasses = LinkedHashSet<String>() // pass ids that fired, across all rounds, in first-fire order
     var harvest = LpHarvestReport() // the LP harvest's own contribution, summed over rounds
+    // Presolve's infeasibility verdict, taken from [Presolved.infeasible] (the incremental path defers
+    // the materialized problem's lazy bake past presolve timing, so this must not force `current.baked`).
+    var infeasible = false
     var round = 0
     while (round++ < MAX_PRESOLVE_HARVEST_ROUNDS && !cancellation()) {
         val pre = Presolver.run(current, config, context, cancellation)
-        val harvestResult = harvestParams?.let { lpHarvestReporting(pre.problem, objective, it, cancellation) }
+        infeasible = infeasible || pre.infeasible
+        val harvestResult = harvestParams?.let {
+            lpHarvestReporting(pre.problem, objective, it, bakeConfig, cancellation)
+        }
         val harvested = harvestResult?.problem ?: pre.problem
         // Neither presolve nor the harvest changed anything this round → fixpoint.
         if (pre.problem === current && harvested === pre.problem) break
@@ -307,7 +321,9 @@ internal fun Solvable.presolved(
     val presolveStats = PresolveStats(
         passes = passes,
         constraintsRemoved = problem.factors.size - current.factors.size,
-        infeasible = current.baked is PropagationResult.Unsat,
+        // From presolve's own verdict (or an LP root-infeasibility), not a forced `current.baked` — the
+        // materialized problem's lazy bake stays out of the presolve timing window.
+        infeasible = infeasible || harvest.rootInfeasible,
         lpHarvest = harvest.takeUnless { it.isEmpty },
     )
     val reconstruct: (Sample) -> Sample = { sample -> reconstructs.foldRight(sample) { f, acc -> f(acc) } }

klause/src/commonMain/kotlin/com/eignex/klause/backtrack/Search.kt

@@ -161,8 +161,9 @@ internal fun BacktrackSolver.driveSearch(
     // trail is at root, so their bound atoms are no longer all-false. Null when learning is off.
     lpNogoods: LpNogoodPool? = null,
 ): Sequence<SearchOutcome> = sequence {
-    if (problem.baked is PropagationResult.Unsat) {
-        yield(SearchOutcome.Exhausted(coreOf(problem.baked)))
+    val baked = problem.baked
+    if (baked is PropagationResult.Unsat) {
+        yield(SearchOutcome.Exhausted(coreOf(baked)))
         return@sequence
     }
     val session = PropagationSession(problem)

klause/src/commonMain/kotlin/com/eignex/klause/backtrack/lp/LpHarvest.kt

@@ -4,6 +4,8 @@ import com.eignex.klause.backtrack.BacktrackParams
 import com.eignex.klause.factor.arithmetic.Linear
 import com.eignex.klause.factor.arithmetic.LinearOp
 import com.eignex.klause.factor.bool.Clause
+import com.eignex.klause.presolve.BakeConfig
+import com.eignex.klause.presolve.RootBaker
 import com.eignex.klause.solver.Cancellation
 import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.Lit
@@ -43,8 +45,9 @@ fun lpHarvest(
     problem: Problem,
     objective: LinearObjective,
     params: BacktrackParams,
+    bakeConfig: BakeConfig = BakeConfig.NONE,
     cancellation: Cancellation = Cancellation.Never,
-): Problem = lpHarvestReporting(problem, objective, params, cancellation).problem
+): Problem = lpHarvestReporting(problem, objective, params, bakeConfig, cancellation).problem
 
 /** [lpHarvest]'s transformed [problem] paired with the [report] of what the LP harvest contributed. */
 class LpHarvestResult(val problem: Problem, val report: LpHarvestReport)
@@ -56,14 +59,15 @@ fun lpHarvestReporting(
     problem: Problem,
     objective: LinearObjective,
     params: BacktrackParams,
+    bakeConfig: BakeConfig = BakeConfig.NONE,
     cancellation: Cancellation = Cancellation.Never,
 ): LpHarvestResult {
     val engine = LpEngine(problem, objective, params, SolveStatsSink(backend = "lp-harvest"))
     if (engine.lpRelaxer == null) return LpHarvestResult(problem, LpHarvestReport())
     // A certified-infeasible root relaxation proves the whole problem has no solution; fold it in as an
     // explicit contradiction so the problem bakes Unsat and every backend short-circuits.
     if (engine.rootInfeasible(cancellation)) {
-        return LpHarvestResult(provenInfeasible(problem), LpHarvestReport(rootInfeasible = true))
+        return LpHarvestResult(provenInfeasible(problem, bakeConfig), LpHarvestReport(rootInfeasible = true))
     }
     val plan = engine.params.lpPlan
     if (!plan.variableShaving && !plan.objectiveShaving) return LpHarvestResult(problem, LpHarvestReport())
@@ -125,17 +129,14 @@ fun lpHarvestReporting(
     } else {
         (problem.factors.filterIndexed { idx, _ -> idx !in redundant } + equalities).toTypedArray()
     }
-    val transformed = Problem(
-        numBoolVars = problem.numBoolVars,
-        numIntVars = problem.numIntVars,
-        intDomains = domains,
-        factors = factors,
-        probeFailedLiterals = problem.probeFailedLiterals,
-        probeIntBounds = problem.probeIntBounds,
-        probeIntHoles = problem.probeIntHoles,
-        probeBudgetPerVar = problem.probeBudgetPerVar,
-        probeTotalBudget = problem.probeTotalBudget,
-        probeSeed = problem.probeSeed,
+    val transformed = RootBaker.reseed(
+        Problem(
+            numBoolVars = problem.numBoolVars,
+            numIntVars = problem.numIntVars,
+            intDomains = domains,
+            factors = factors,
+        ),
+        bakeConfig,
     )
     return LpHarvestResult(transformed, report)
 }
@@ -147,7 +148,7 @@ fun lpHarvestReporting(
  * the conflict is witnessed without depending on the LP proof being re-derivable downstream. Sound: an
  * infeasible problem has no solutions, and the relaxation infeasibility certifies there are none.
  */
-private fun provenInfeasible(problem: Problem): Problem {
+private fun provenInfeasible(problem: Problem, bakeConfig: BakeConfig): Problem {
     val factors = ArrayList<Factor>(problem.factors.size + 2)
     factors.addAll(problem.factors)
     when {
@@ -165,16 +166,13 @@ private fun provenInfeasible(problem: Problem): Problem {
 
         else -> return problem // no variable to pin a contradiction on (a variable-free problem)
     }
-    return Problem(
-        numBoolVars = problem.numBoolVars,
-        numIntVars = problem.numIntVars,
-        intDomains = problem.intDomains.copyOf(),
-        factors = factors,
-        probeFailedLiterals = problem.probeFailedLiterals,
-        probeIntBounds = problem.probeIntBounds,
-        probeIntHoles = problem.probeIntHoles,
-        probeBudgetPerVar = problem.probeBudgetPerVar,
-        probeTotalBudget = problem.probeTotalBudget,
-        probeSeed = problem.probeSeed,
+    return RootBaker.reseed(
+        Problem(
+            numBoolVars = problem.numBoolVars,
+            numIntVars = problem.numIntVars,
+            intDomains = problem.intDomains.copyOf(),
+            factors = factors,
+        ),
+        bakeConfig,
     )
 }

klause/src/commonMain/kotlin/com/eignex/klause/compile/Compiler.kt

@@ -60,8 +60,6 @@ import com.eignex.klause.model.SubcircuitExpr
 import com.eignex.klause.model.SymmetricAllDifferent
 import com.eignex.klause.model.TableConstraint
 import com.eignex.klause.model.XorExpr
-import com.eignex.klause.presolve.PresolveContext
-import com.eignex.klause.presolve.PresolvePass
 import com.eignex.klause.schema.VariableSchema
 import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.IntDomain
@@ -492,21 +490,15 @@ private fun Lowering.run(def: SchemaDef<SchemaEntry>): CompiledProblem {
     // contribute dead-value symmetry. Gated by config so it can be turned off.
     if (config.pinAbsentOptVars) emitOptVarPins(def)
 
-    // Construction-time SAC probes are resolved from the presolve config (solution-preserving, so
-    // intent-independent — resolved under EMPTY). Holes imply bounds.
-    val presolve = config.presolveConfig()
-    val holes = presolve.resolved(PresolvePass.PROBE_INT_HOLES, PresolveContext.EMPTY)
+    // The compiler builds a plain base-baked [Problem]; the SAC / failed-literal probing tiers, resolved
+    // from the presolve config, now run in the presolve lane via [RootBaker] (kernel → presolve would
+    // cycle). The presolve pipeline reads the same config through [BakeConfig.from].
     return CompiledProblem(
         problem = Problem(
             numBoolVars = numBoolVars,
             numIntVars = numIntVars,
             intDomains = intDomains.toTypedArray(),
             factors = factors.toTypedArray(),
-            probeFailedLiterals = presolve.resolved(PresolvePass.PROBE_FAILED_LITERALS, PresolveContext.EMPTY),
-            probeIntBounds = holes || presolve.resolved(PresolvePass.PROBE_INT_BOUNDS, PresolveContext.EMPTY),
-            probeIntHoles = holes,
-            probeBudgetPerVar = presolve.probeBudgetPerVar(),
-            probeTotalBudget = presolve.probeTotalBudget(),
         ),
         boolVarIdByName = boolVarIdByName.toMap(),
         intVarIdByName = intVarIdByName.toMap(),

klause/src/commonMain/kotlin/com/eignex/klause/formats/flatzinc/FlatZincCompiler.kt

@@ -3,10 +3,7 @@ import com.eignex.klause.config.DEFAULT_FLOAT_BUCKETS
 import com.eignex.klause.config.DEFAULT_FLOAT_SCALE
 import com.eignex.klause.config.DEFAULT_UNBOUNDED_INT_HI
 import com.eignex.klause.config.DEFAULT_UNBOUNDED_INT_LO
-import com.eignex.klause.config.KlauseConfig
 import com.eignex.klause.factor.bool.Clause
-import com.eignex.klause.presolve.PresolveContext
-import com.eignex.klause.presolve.PresolvePass
 import com.eignex.klause.solver.Cancellation
 import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.IntDomain
@@ -53,23 +50,18 @@ internal class FlatZincCompiler(
             if (redundant || symmetry) for (i in before until factors.size) impliedFactorIds.add(i)
         }
         val solveDirective = compileSolve()
-        val presolve = KlauseConfig.current.presolveConfig()
-        val holes = presolve.resolved(PresolvePass.PROBE_INT_HOLES, PresolveContext.EMPTY)
         val impliedFactorMask = if (impliedFactorIds.isEmpty()) {
             null
         } else {
             BooleanArray(factors.size).also { for (i in impliedFactorIds) it[i] = true }
         }
+        // A plain base-baked [Problem]; the SAC / failed-literal probing resolved from the presolve
+        // config runs later in the presolve lane via [RootBaker] (the kernel never probes itself).
         val problem = Problem(
             numBoolVars = numBoolVars,
             numIntVars = intDomains.size,
             intDomains = intDomains.toTypedArray(),
             factors = factors.toTypedArray(),
-            probeFailedLiterals = presolve.resolved(PresolvePass.PROBE_FAILED_LITERALS, PresolveContext.EMPTY),
-            probeIntBounds = holes || presolve.resolved(PresolvePass.PROBE_INT_BOUNDS, PresolveContext.EMPTY),
-            probeIntHoles = holes,
-            probeBudgetPerVar = presolve.probeBudgetPerVar(),
-            probeTotalBudget = presolve.probeTotalBudget(),
             cancellation = cancellation,
             impliedFactorMask = impliedFactorMask,
             hasSymmetryBreaking = hasSymmetryBreaking,

klause/src/commonMain/kotlin/com/eignex/klause/presolve/AffineElimination.kt

@@ -42,20 +42,27 @@ internal object AffineSingletons {
         problem: Problem,
         objectiveIntVars: Set<Int> = emptySet(),
         cancellation: Cancellation = Cancellation.Never,
-    ): AffineElimination {
-        if (problem.numIntVars == 0) return AffineElimination(problem, emptyList())
+        sharedIntOcc: SharedIntOccurrence? = null,
+    ): PassDelta {
+        if (problem.numIntVars == 0) return PassDelta()
         var factors = problem.factors.toList()
         val eliminated = BooleanArray(problem.numIntVars)
         val subs = ArrayList<AffineSub>()
+        // The session-maintained index matches the pristine input factor order, so the first candidate
+        // search reads it instead of rebuilding an O(factors) index; once [foldOutVariable] rewrites the
+        // list the intra-pass fixpoint rebuilds a local one (the win is the per-round search rebuild).
+        var occ = sharedIntOcc?.let { OccurrenceIndex(it.offsets, it.flat) }
+            ?: buildOccurrenceIndex(factors, eliminated.size)
         // Each elimination rescans and re-indexes the factor set and folds the pivot into every factor
         // mentioning it; on a model with a wide row absorbing eliminations the loop turns quadratic.
         // Poll the budget so it stops with the eliminations made so far — sound (the remaining
         // affine-defined variables simply stay and are solved directly).
         while (!cancellation()) {
-            val cand = findAffineCandidate(factors, eliminated, objectiveIntVars) ?: break
+            val cand = findAffineCandidate(factors, occ, eliminated, objectiveIntVars) ?: break
             factors = foldOutVariable(problem, factors, cand)
             eliminated[cand.x] = true
             subs.add(AffineSub(cand.x, cand.constTerm, cand.termVars, cand.termCoeffs))
+            occ = buildOccurrenceIndex(factors, eliminated.size)
         }
         // Residue-class doubletons (#522): a 2-term `a·x + b·y = c` with no unit pivot, where `x` is
         // contained, determines `x = (c − b·y)/a` only for the `y` values keeping it an in-domain
@@ -64,14 +71,18 @@ internal object AffineSingletons {
         // is always a surviving variable.
         val domains = problem.intDomains.copyOf()
         while (!cancellation()) {
-            val r = findResidueCandidate(factors, eliminated, objectiveIntVars, domains) ?: break
+            val r = findResidueCandidate(factors, occ, eliminated, objectiveIntVars, domains) ?: break
             factors = factors.filterIndexed { i, _ -> i != r.defIdx }
             domains[r.y] = r.restrictedY
             eliminated[r.x] = true
             subs.add(AffineSub(r.x, r.constTerm, intArrayOf(r.y), intArrayOf(r.coeffY), divisor = r.divisor))
+            occ = buildOccurrenceIndex(factors, eliminated.size)
         }
-        if (subs.isEmpty()) return AffineElimination(problem, emptyList())
-        return AffineElimination(PresolveShared.rebuildProblem(problem, factors, domains), subs)
+        if (subs.isEmpty()) return PassDelta()
+        // The eliminations rebuilt the factor list in place; recover the delta against the input by
+        // identity — every survivor is === an input factor, so the drops are the inputs absent from
+        // [factors] and the adds are the factors [foldOutVariable] introduced (rewrites + domain bounds).
+        return PresolveShared.identityDelta(problem.factors, factors, domains, AffineElimination(subs)::reconstruct)
     }
 
     /** Cap on a residue partner's domain span: scanning each value to build the restricted domain is
@@ -92,11 +103,11 @@ internal object AffineSingletons {
 
     private fun findResidueCandidate(
         factors: List<Factor>,
+        occ: OccurrenceIndex,
         eliminated: BooleanArray,
         objectiveIntVars: Set<Int>,
         domains: Array<IntDomain>,
     ): ResidueCandidate? {
-        val occ = buildOccurrenceIndex(factors, eliminated.size)
         for (di in factors.indices) {
             val f = factors[di]
             if (f !is Linear || f.op != LinearOp.EQ || f.vars.size != 2) continue
@@ -167,16 +178,16 @@ internal object AffineSingletons {
 
     private fun findAffineCandidate(
         factors: List<Factor>,
+        occ: OccurrenceIndex,
         eliminated: BooleanArray,
         objectiveIntVars: Set<Int>,
     ): AffineCandidate? {
-        // Occurrence index (variable id → the factor indices that mention it), built once per scan so
+        // [occ] maps variable id → the factor indices that mention it (CSR: counts → offsets → flat), so
         // the per-candidate "where else does x occur" checks are O(occurrences-of-x) instead of a fresh
-        // O(factors) linear scan each. On a large model that quadratic scan dominated affine
-        // elimination; the index makes it linear in x's actual degree. Result-identical — purely a
-        // faster lookup of the same factor membership. CSR layout (counts → offsets → flat) avoids a
-        // per-variable list allocation, which matters when there are hundreds of thousands of variables.
-        val occ = buildOccurrenceIndex(factors, eliminated.size)
+        // O(factors) linear scan each. On a large model that quadratic scan dominated affine elimination;
+        // the index makes it linear in x's actual degree. The caller supplies the session-maintained index
+        // for the pristine input and a freshly-built one after each elimination — result-identical, purely
+        // a faster lookup of the same factor membership.
         for (di in factors.indices) {
             val f = factors[di]
             if (f !is Linear || f.op != LinearOp.EQ || f.vars.size < 2) continue
@@ -362,16 +373,12 @@ internal class AffineSub(
 )
 
 /**
- * Reduced problem from [Presolve.eliminateAffineSingletons] plus the data to rebuild the
- * eliminated variables. Solve [problem], then pass the solution through [reconstruct] to recover
- * a solution of the original problem.
+ * The affine eliminations [Presolve.eliminateAffineSingletons] made, holding the data to rebuild the
+ * eliminated variables. Pass a solution of the reduced problem through [reconstruct] to recover a
+ * solution of the original.
  */
-class AffineElimination internal constructor(
-    /** The problem with affine-defined variables eliminated. */
-    val problem: Problem,
-    private val subs: List<AffineSub>,
-) {
-    /** Recover the eliminated variables in a solution [sample] of [problem]. Processed in reverse
+internal class AffineElimination(private val subs: List<AffineSub>) {
+    /** Recover the eliminated variables in a solution [sample] of the reduced problem. Processed in reverse
      *  elimination order: an eliminated `x` may depend on a `y` eliminated later (a chain), and a
      *  later elimination never depends on an earlier one (the candidate scan skips already-eliminated
      *  partners), so reverse order guarantees every `y` is reconstructed before the `x` that reads it. */