diff --git a/klause-cli/src/commonMain/kotlin/com/eignex/klause/cli/CliMode.kt b/klause-cli/src/commonMain/kotlin/com/eignex/klause/cli/CliMode.kt
index 662aaba13..5edd101cf 100644
--- a/klause-cli/src/commonMain/kotlin/com/eignex/klause/cli/CliMode.kt
+++ b/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) } }
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/backtrack/Search.kt b/klause/src/commonMain/kotlin/com/eignex/klause/backtrack/Search.kt
index 9c58038cd..b01b3dc98 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/backtrack/Search.kt
+++ b/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)
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/backtrack/lp/LpHarvest.kt b/klause/src/commonMain/kotlin/com/eignex/klause/backtrack/lp/LpHarvest.kt
index 9d6e1a13e..9ac7c7024 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/backtrack/lp/LpHarvest.kt
+++ b/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,6 +59,7 @@ 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"))
@@ -63,7 +67,7 @@ fun lpHarvestReporting(
     // 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,
     )
 }
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/compile/Compiler.kt b/klause/src/commonMain/kotlin/com/eignex/klause/compile/Compiler.kt
index 209eca542..d7c0e9c10 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/compile/Compiler.kt
+++ b/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(),
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/formats/flatzinc/FlatZincCompiler.kt b/klause/src/commonMain/kotlin/com/eignex/klause/formats/flatzinc/FlatZincCompiler.kt
index 05712ea3b..e1208df14 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/formats/flatzinc/FlatZincCompiler.kt
+++ b/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,
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/AffineElimination.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/AffineElimination.kt
index b4751717b..9269c0de4 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/AffineElimination.kt
+++ b/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. */
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/BakeConfig.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/BakeConfig.kt
new file mode 100644
index 000000000..c9a933586
--- /dev/null
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/BakeConfig.kt
@@ -0,0 +1,67 @@
+package com.eignex.klause.presolve
+
+/**
+ * Which root-bake probing tiers [RootBaker.bake] runs, and their budgets. Formerly the six `probe*`
+ * parameters on the kernel `Problem`; now threaded through the presolve / backtrack lanes so the kernel
+ * carries no probing policy. [NONE] disables all probing (the common case — a plain [RootBaker.bake] is
+ * then a no-op returning the base bake).
+ */
+class BakeConfig(
+    /**
+     * Failed-literal probing. When `true`, every free bool variable is tested with both polarities: if
+     * pinning one polarity propagates Unsat, the other polarity is forced. Iterated to a fixed point.
+     */
+    val probeFailedLiterals: Boolean = false,
+    /**
+     * Bound-SAC (singleton arc consistency). After [probeFailedLiterals] settles, every int var with a
+     * multi-value domain has its min and max probed: pin the bound, propagate, and if Unsat, tighten the
+     * bound by one and loop. Captures bound-level deductions the per-call propagator misses.
+     */
+    val probeIntBounds: Boolean = false,
+    /**
+     * Interior-hole SAC. Builds on [probeIntBounds]: after bound-SAC settles, each multi-value int var
+     * has its interior values (strictly between current min and max) probed; on Unsat the value is
+     * recorded as an interior hole. Implies [probeIntBounds].
+     */
+    val probeIntHoles: Boolean = false,
+    /**
+     * Cap on per-var probe calls during SAC. After this many `propagate` calls targeting one var (across
+     * both bound and hole probing), the loop stops probing that var. Unlimited by default.
+     */
+    val probeBudgetPerVar: Int = Int.MAX_VALUE,
+    /**
+     * Cap on total probe calls across all vars and all SAC passes. Once exceeded, the SAC loops exit
+     * gracefully with whatever tightenings they've accumulated. Unlimited by default.
+     */
+    val probeTotalBudget: Int = Int.MAX_VALUE,
+    /**
+     * Seed for the RNG that breaks ties in the wdeg-weighted SAC probe order. Deterministic for a given
+     * seed.
+     */
+    val probeSeed: Long = 0L,
+) {
+    /** True iff any probing tier is enabled — when false, [RootBaker.bake] returns the base bake as-is. */
+    val anyEnabled: Boolean get() = probeFailedLiterals || probeIntBounds || probeIntHoles
+
+    /** Shared config and the [PresolveConfig]-derived factory. */
+    companion object {
+        /** No probing — the kernel base bake stands alone. */
+        val NONE: BakeConfig = BakeConfig()
+
+        /**
+         * Resolve the root-bake probing tiers from a [PresolveConfig] under [context]. The construction-
+         * time SAC probes are solution-preserving, so they resolve independently of query intent (the
+         * compile sites use [PresolveContext.EMPTY]); interior-hole SAC implies bound SAC.
+         */
+        fun from(config: PresolveConfig, context: PresolveContext = PresolveContext.EMPTY): BakeConfig {
+            val holes = config.resolved(PresolvePass.PROBE_INT_HOLES, context)
+            return BakeConfig(
+                probeFailedLiterals = config.resolved(PresolvePass.PROBE_FAILED_LITERALS, context),
+                probeIntBounds = holes || config.resolved(PresolvePass.PROBE_INT_BOUNDS, context),
+                probeIntHoles = holes,
+                probeBudgetPerVar = config.probeBudgetPerVar(),
+                probeTotalBudget = config.probeTotalBudget(),
+            )
+        }
+    }
+}
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/CoefficientStrengthening.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/CoefficientStrengthening.kt
index 33e86f34b..fa0446540 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/CoefficientStrengthening.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/CoefficientStrengthening.kt
@@ -9,6 +9,7 @@ import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Lit
 import com.eignex.klause.solver.Problem
+import com.eignex.klause.util.IntArrayList
 
 internal object CoefficientStrengthening {
 
@@ -27,39 +28,32 @@ internal object CoefficientStrengthening {
      * Exact (feasible-set-preserving) and it tightens the LP relaxation the bound participates in.
      * Other factor types pass through untouched.
      */
-    fun strengthenCoefficients(problem: Problem): Problem {
-        val out = ArrayList<Factor>(problem.factors.size)
-        var changed = false
-        for (factor in problem.factors) {
+    fun strengthenCoefficients(problem: Problem): PassDelta {
+        val dropped = IntArrayList()
+        val added = ArrayList<Factor>()
+        problem.factors.forEachIndexed { i, factor ->
             // An equality whose coefficient GCD does not divide its bound can never hold; replace it by
             // an explicit contradiction (the original is redundant once the problem is infeasible).
             val contradiction = equalityContradiction(factor, problem.intDomains)
             if (contradiction != null) {
-                out.addAll(contradiction)
-                changed = true
-                continue
+                dropped.add(i)
+                added.addAll(contradiction)
+                return@forEachIndexed
             }
             val rewritten = when (factor) {
                 is Linear -> strengthenLinear(factor, problem.intDomains)
                 is PseudoBoolean -> strengthenPb(factor)
                 else -> factor
             }
-            if (rewritten !== factor) changed = true
-            if (rewritten != null) out.add(rewritten)
+            // A rewrite replaces the input factor; a `null` drops it (always satisfied); an unchanged
+            // factor contributes nothing to the delta.
+            if (rewritten !== factor) {
+                dropped.add(i)
+                if (rewritten != null) added.add(rewritten)
+            }
         }
-        if (!changed) return problem
-        return Problem(
-            numBoolVars = problem.numBoolVars,
-            numIntVars = problem.numIntVars,
-            intDomains = problem.intDomains.copyOf(),
-            factors = out,
-            probeFailedLiterals = problem.probeFailedLiterals,
-            probeIntBounds = problem.probeIntBounds,
-            probeIntHoles = problem.probeIntHoles,
-            probeBudgetPerVar = problem.probeBudgetPerVar,
-            probeTotalBudget = problem.probeTotalBudget,
-            probeSeed = problem.probeSeed,
-        )
+        if (dropped.isEmpty()) return PassDelta()
+        return PassDelta(dropped.toIntArray(), added)
     }
 
     /** The factors that make the model infeasible when [factor] is an equality whose coefficient GCD
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DominatedVariables.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DominatedVariables.kt
index 1993d63a0..f6607a807 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DominatedVariables.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DominatedVariables.kt
@@ -46,7 +46,7 @@ internal object DominatedVariables {
         problem: Problem,
         objectiveIntCoeffs: Map<Int, Long>,
         objectiveBoolCoeffs: Map<Int, Long> = emptyMap(),
-    ): Problem {
+    ): PassDelta {
         val n = problem.numIntVars
         val downSafe = BooleanArray(n) { true }
         val upSafe = BooleanArray(n) { true }
@@ -76,7 +76,7 @@ internal object DominatedVariables {
             }
             markBoolSafety(f, trueSafe, falseSafe, boolEligible, alreadyPinned)
         }
-        var changed = false
+        var domainsNarrowed = false
         val domains = problem.intDomains.copyOf()
         for (v in 0 until n) {
             if (!intEligible[v]) continue
@@ -86,12 +86,12 @@ internal object DominatedVariables {
             when {
                 downSafe[v] && c >= 0L -> {
                     domains[v] = IntDomain(d.min, d.min)
-                    changed = true
+                    domainsNarrowed = true
                 }
 
                 upSafe[v] && c <= 0L -> {
                     domains[v] = IntDomain(d.max, d.max)
-                    changed = true
+                    domainsNarrowed = true
                 }
             }
         }
@@ -104,10 +104,11 @@ internal object DominatedVariables {
                 falseSafe[b] && c >= 0L -> extra.add(Clause(intArrayOf(Lit.make(b, false))))
                 else -> continue
             }
-            changed = true
         }
-        if (!changed) return problem
-        return PresolveShared.rebuildProblem(problem, problem.factors.toList() + extra, domains)
+        if (!domainsNarrowed && extra.isEmpty()) return PassDelta()
+        // Carry the pinned domains only when a pin actually narrowed one, so a bool-only fixing yields a
+        // pure-add delta the fixpoint check reads correctly.
+        return PassDelta(addedFactors = extra, domains = if (domainsNarrowed) domains else null)
     }
 
     /** Fold [f]'s contribution to the Boolean pure-literal safety analysis (#469/#470). A bool var is
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DuplicateColumns.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DuplicateColumns.kt
index ee4176e3b..069da3ddc 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DuplicateColumns.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/DuplicateColumns.kt
@@ -5,6 +5,7 @@ import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Problem
 import com.eignex.klause.solver.Sample
+import com.eignex.klause.util.IntArrayList
 import com.eignex.klause.util.MutableIntIntMap
 
 internal object DuplicateColumns {
@@ -45,10 +46,14 @@ internal object DuplicateColumns {
      * re-signs against the widened aggregate and is picked up on a later round, keeping every merge a
      * two-variable aggregate over *declared* domains that the contiguous split reconstructs exactly.
      */
-    fun mergeDuplicateColumns(problem: Problem, objectiveIntVars: Set<Int> = emptySet()): DuplicateColumnMerge {
-        if (problem.numIntVars < 2) return DuplicateColumnMerge(problem, emptyList())
-        val eligible = eligibleColumns(problem, objectiveIntVars)
-        val signatures = columnSignatures(problem, eligible)
+    fun mergeDuplicateColumns(
+        problem: Problem,
+        objectiveIntVars: Set<Int> = emptySet(),
+        sharedIntOcc: SharedIntOccurrence? = null,
+    ): PassDelta {
+        if (problem.numIntVars < 2) return PassDelta()
+        val eligible = eligibleColumns(problem, objectiveIntVars, sharedIntOcc)
+        val signatures = columnSignatures(problem, eligible, sharedIntOcc)
         // Group eligible variables by column signature; equal signatures are duplicate columns. Fold
         // at most one duplicate into each representative this pass (a third re-signs next round).
         val repBySignature = HashMap<List<Long>, Int>()
@@ -72,17 +77,29 @@ internal object DuplicateColumns {
                 repConsumed.add(rep)
             }
         }
-        if (merges.isEmpty()) return DuplicateColumnMerge(problem, emptyList())
+        if (merges.isEmpty()) return PassDelta()
 
         val keepOf = IntArray(problem.numIntVars) { it } // drop → its aggregate representative
         val domains = problem.intDomains.copyOf()
         for (m in merges) {
             keepOf[m.drop] = m.keep
             val keep = domains[m.keep]
+            // Widen the aggregate to the Minkowski sum; the session must reseed on this widen, so it flows
+            // through [PassDelta.domains].
             domains[m.keep] = IntDomain(keep.min + m.dropDomain.min, keep.max + m.dropDomain.max)
         }
-        val factors = problem.factors.map { aggregateColumns(it, keepOf) }
-        return DuplicateColumnMerge(PresolveShared.rebuildProblem(problem, factors, domains), merges)
+        // Each row is rewritten in place; the changed ones become drop+add, the untouched ones (identity
+        // unchanged) contribute nothing.
+        val dropped = IntArrayList()
+        val added = ArrayList<Factor>()
+        problem.factors.forEachIndexed { i, f ->
+            val rewritten = aggregateColumns(f, keepOf)
+            if (rewritten !== f) {
+                dropped.add(i)
+                added.add(rewritten)
+            }
+        }
+        return PassDelta(dropped.toIntArray(), added, domains, DuplicateColumnMerge(merges)::reconstruct)
     }
 
     /** [factor] with every dropped duplicate column folded into its representative: in a [Linear] row,
@@ -106,11 +123,29 @@ internal object DuplicateColumns {
 
     /** Per-variable eligibility: every occurrence is a [Linear] factor (a global / reified row reads a
      *  variable value-wise, not as a column coefficient), the domain is contiguous (the reconstruction
-     *  split must not land in a hole), and the variable is not read by the objective. */
-    private fun eligibleColumns(problem: Problem, objectiveIntVars: Set<Int>): BooleanArray {
+     *  split must not land in a hole), and the variable is not read by the objective. With the
+     *  session-maintained [occ] the non-[Linear] test is a per-var walk of its factors; otherwise the
+     *  factor list is scanned once to mark every variable a non-[Linear] factor mentions. */
+    private fun eligibleColumns(
+        problem: Problem,
+        objectiveIntVars: Set<Int>,
+        occ: SharedIntOccurrence?,
+    ): BooleanArray {
         val eligible = BooleanArray(problem.numIntVars) { v ->
             v !in objectiveIntVars && problem.intDomains[v].isContiguous()
         }
+        if (occ != null) {
+            for (v in 0 until problem.numIntVars) {
+                if (!eligible[v]) continue
+                for (k in occ.offsets[v] until occ.offsets[v + 1]) {
+                    if (problem.factors[occ.flat[k]] !is Linear) {
+                        eligible[v] = false
+                        break
+                    }
+                }
+            }
+            return eligible
+        }
         for (f in problem.factors) {
             if (f is Linear) continue
             for (v in f.intVars) eligible[v] = false
@@ -122,8 +157,28 @@ internal object DuplicateColumns {
      *  with its coefficient there, sorted by factor id. Two eligible variables share a signature iff
      *  they occur in exactly the same factors with the same coefficient in each — duplicate columns.
      *  Ineligible variables, and variables in no factor, get a `null` signature and never match. */
-    private fun columnSignatures(problem: Problem, eligible: BooleanArray): Array<List<Long>?> {
+    private fun columnSignatures(
+        problem: Problem,
+        eligible: BooleanArray,
+        occ: SharedIntOccurrence?,
+    ): Array<List<Long>?> {
         val entries = Array(problem.numIntVars) { if (eligible[it]) ArrayList<Long>() else null }
+        if (occ != null) {
+            // Per eligible variable, walk its factors from the shared index in ascending factor id (the
+            // CSR flat order) — the same order the factor scan below appends — so the signature list is
+            // identical. Every occurrence of an eligible variable is a [Linear] (a non-[Linear] one made
+            // it ineligible), so its coefficient is always present in that row.
+            for (v in 0 until problem.numIntVars) {
+                val list = entries[v] ?: continue
+                for (k in occ.offsets[v] until occ.offsets[v + 1]) {
+                    val fid = occ.flat[k]
+                    val f = problem.factors[fid] as Linear
+                    list.add(fid.toLong())
+                    list.add(f.coeffs[f.vars.indexOf(v)].toLong())
+                }
+            }
+            return Array(problem.numIntVars) { entries[it]?.takeIf { e -> e.isNotEmpty() } }
+        }
         problem.factors.forEachIndexed { fid, f ->
             if (f !is Linear) return@forEachIndexed
             val coeffByVar = MutableIntIntMap(f.vars.size)
@@ -147,16 +202,12 @@ internal object DuplicateColumns {
 internal class ColumnMerge(val keep: Int, val drop: Int, val keepDomain: IntDomain, val dropDomain: IntDomain)
 
 /**
- * Reduced problem from [Presolve.mergeDuplicateColumns] plus the data to split each aggregate
- * variable back into its two originals. Solve [problem], then pass the solution through
- * [reconstruct] to recover a solution of the original problem.
+ * The duplicate-column aggregations [Presolve.mergeDuplicateColumns] made, holding the data to split
+ * each aggregate variable back into its two originals. Pass a solution of the reduced problem through
+ * [reconstruct] to recover a solution of the original.
  */
-class DuplicateColumnMerge internal constructor(
-    /** The problem with duplicate columns aggregated. */
-    val problem: Problem,
-    private val merges: List<ColumnMerge>,
-) {
-    /** Recover the dropped variables in a solution [sample] of [problem]. The aggregate `keep` holds
+internal class DuplicateColumnMerge(private val merges: List<ColumnMerge>) {
+    /** Recover the dropped variables in a solution [sample] of the reduced problem. The aggregate `keep` holds
      *  `z = x + y`; a feasible split needs `x ∈ [min(x), max(x)]` and `y = z − x ∈ [min(y), max(y)]`,
      *  i.e. `x ∈ [max(min(x), z − max(y)), min(max(x), z − min(y))]`, non-empty for every `z` the
      *  aggregate admits when both originals are contiguous. Take its lower end. Each merge has a
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/ImplicationGraph.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/ImplicationGraph.kt
index d758a4c8e..65d6888b1 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/ImplicationGraph.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/ImplicationGraph.kt
@@ -41,17 +41,24 @@ internal object ImplicationGraph {
         maxCandidates: Int,
         cancellation: Cancellation,
         objectiveBoolVars: Set<Int> = emptySet(),
-    ): ImplicationReduction {
-        if (problem.numBoolVars == 0) return ImplicationReduction(problem, emptyList())
+    ): PassDelta {
+        if (problem.numBoolVars == 0) return PassDelta()
 
         val implications = harvestImplications(problem, maxCandidates, cancellation)
         val merges = equivalentVariableMerges(problem.numBoolVars, implications, objectiveBoolVars)
 
-        val substituted = if (merges.isEmpty()) problem else applyMerges(problem, merges)
-        val reduced = dropTransitivelyRedundantBinaries(substituted)
+        val original = problem.factors.asList()
+        val substituted = if (merges.isEmpty()) original else applyMerges(problem, merges)
+        val reduced = dropTransitivelyRedundantBinaries(problem, substituted)
 
-        if (reduced === problem) return ImplicationReduction(problem, emptyList())
-        return ImplicationReduction(reduced, merges)
+        // A rename/drop leaves survivors identity-equal to inputs; a pure no-op keeps the same list, which
+        // [identityDelta] renders as an empty delta (== the fresh path's `=== problem` fixpoint signal).
+        if (merges.isEmpty() && reduced === original) return PassDelta()
+        return PresolveShared.identityDelta(
+            problem.factors,
+            reduced,
+            reconstruct = ImplicationReduction(merges)::reconstruct,
+        )
     }
 
     /**
@@ -149,7 +156,7 @@ internal object ImplicationGraph {
      *  binary clause that the rename turns into a tautology (`r ⇒ r`). Bool variable count is
      *  preserved; a merged variable simply stops appearing in any factor and is rebuilt on the way
      *  back. */
-    private fun applyMerges(problem: Problem, merges: List<BoolMerge>): Problem {
+    private fun applyMerges(problem: Problem, merges: List<BoolMerge>): List<Factor> {
         val boolMap = IntArray(problem.numBoolVars) { it }
         for (m in merges) boolMap[m.from] = m.into
         val intMap = IntArray(problem.numIntVars) { it }
@@ -159,7 +166,7 @@ internal object ImplicationGraph {
             if (remapped is Clause && isTautology(remapped)) continue
             out.add(remapped)
         }
-        return PresolveShared.rebuildProblem(problem, out)
+        return out
     }
 
     /** A clause that holds in every assignment because some variable appears in both polarities. */
@@ -179,34 +186,34 @@ internal object ImplicationGraph {
      * redundant exactly when `b` is reachable from `a` over the remaining edges without using this
      * clause's own two edges — propagation then still derives `b` from `a`, so satisfiability and the
      * optimum are untouched. Non-binary factors and unit clauses are always kept; when nothing is
-     * dropped the input problem is returned unchanged (the pass's no-op signal).
+     * dropped [factors] is returned unchanged (identity, the pass's no-op signal).
      */
-    private fun dropTransitivelyRedundantBinaries(problem: Problem): Problem {
+    private fun dropTransitivelyRedundantBinaries(problem: Problem, factors: List<Factor>): List<Factor> {
         val binaryIndices = ArrayList<Int>()
-        problem.factors.forEachIndexed { i, f -> if (f is Clause && f.literals.size == 2) binaryIndices.add(i) }
-        if (binaryIndices.size < 2) return problem
+        factors.forEachIndexed { i, f -> if (f is Clause && f.literals.size == 2) binaryIndices.add(i) }
+        if (binaryIndices.size < 2) return factors
 
         val adj = Adjacency(2 * problem.numBoolVars)
         for (i in binaryIndices) {
-            val (a, b) = implicationEdges(problem.factors[i] as Clause)
+            val (a, b) = implicationEdges(factors[i] as Clause)
             adj.addEdge(a.first, a.second)
             adj.addEdge(b.first, b.second)
         }
 
         val drop = HashSet<Int>()
         for (i in binaryIndices) {
-            val clause = problem.factors[i] as Clause
+            val clause = factors[i] as Clause
             val (e1, e2) = implicationEdges(clause)
             // Redundant iff the implication has an alternative path that avoids this clause's own two
             // directed edges. Checking one direction suffices: the contrapositive is reachable iff the
             // forward implication is, so a single source→target search settles the clause.
             if (reachableAvoiding(adj, e1.first, e1.second, e1, e2)) drop.add(i)
         }
-        if (drop.isEmpty()) return problem
+        if (drop.isEmpty()) return factors
 
-        val kept = ArrayList<Factor>(problem.factors.size - drop.size)
-        problem.factors.forEachIndexed { i, f -> if (i !in drop) kept.add(f) }
-        return PresolveShared.rebuildProblem(problem, kept)
+        val kept = ArrayList<Factor>(factors.size - drop.size)
+        factors.forEachIndexed { i, f -> if (i !in drop) kept.add(f) }
+        return kept
     }
 
     /** The two implication edges a binary clause `(p ∨ q)` encodes: `¬p -> q` and `¬q -> p`. */
@@ -333,14 +340,11 @@ internal object ImplicationGraph {
 internal class BoolMerge(val from: Int, val into: Int)
 
 /**
- * Reduced problem from [ImplicationGraph.reduce] plus the data to rebuild merged variables. Solve
- * [problem], then pass the solution through [reconstruct] to recover a solution of the original.
+ * The equivalent-literal merges [ImplicationGraph.reduce] made, holding the data to rebuild merged
+ * variables. Pass a solution of the reduced problem through [reconstruct] to recover a solution of the
+ * original.
  */
-class ImplicationReduction internal constructor(
-    /** The problem with equivalent literals collapsed and redundant binaries dropped. */
-    val problem: Problem,
-    private val merges: List<BoolMerge>,
-) {
+internal class ImplicationReduction(private val merges: List<BoolMerge>) {
     /** Recover each merged variable in a solution [sample] by copying its representative's value.
      *  Representatives are never themselves merged away (the smallest id in a component is the rep and
      *  only larger ids merge into it), so a single forward pass suffices. */
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolve.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolve.kt
index ebf48e686..019725b4f 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolve.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolve.kt
@@ -14,24 +14,26 @@ object Presolve {
 
     /** GCD coefficient strengthening for [com.eignex.klause.factor.arithmetic.Linear] and
      *  pseudo-Boolean constraints. See [CoefficientStrengthening]. */
-    fun strengthenCoefficients(problem: Problem): Problem = CoefficientStrengthening.strengthenCoefficients(problem)
+    fun strengthenCoefficients(problem: Problem): PassDelta = CoefficientStrengthening.strengthenCoefficients(problem)
 
     /** One-shot GF(2) elimination over all xor factors. See [XorUnits]. */
-    fun deriveXorUnits(problem: Problem): Problem = XorUnits.deriveXorUnits(problem)
+    fun deriveXorUnits(problem: Problem): PassDelta = XorUnits.deriveXorUnits(problem)
 
     /** Affine variable elimination. See [AffineSingletons]. */
     fun eliminateAffineSingletons(
         problem: Problem,
         objectiveIntVars: Set<Int> = emptySet(),
         cancellation: Cancellation = Cancellation.Never,
-    ): AffineElimination = AffineSingletons.eliminateAffineSingletons(problem, objectiveIntVars, cancellation)
+        sharedIntOcc: SharedIntOccurrence? = null,
+    ): PassDelta = AffineSingletons.eliminateAffineSingletons(problem, objectiveIntVars, cancellation, sharedIntOcc)
 
     /** Constraint subsumption / redundant-constraint removal. See [RedundantConstraints]. */
-    fun removeRedundantConstraints(problem: Problem): Problem = RedundantConstraints.removeRedundantConstraints(problem)
+    fun removeRedundantConstraints(problem: Problem): PassDelta =
+        RedundantConstraints.removeRedundantConstraints(problem)
 
     /** Per-factor structural self-reduction via [com.eignex.klause.solver.Factor.structuralReduce].
      *  See [StructuralReduction]. */
-    fun reduceStructural(problem: Problem): Problem = StructuralReduction.reduce(problem)
+    fun reduceStructural(problem: Problem): PassDelta = StructuralReduction.reduce(problem)
 
     /** Maximal at-most-one cliques (Lit-encoded, at most one satisfied) recognised from [problem]'s
      *  factors — including those implied by pseudo-Boolean knapsacks — and grown into maximal cliques,
@@ -39,8 +41,11 @@ object Presolve {
     fun amoCliques(problem: Problem): List<Set<Int>> = PresolveShared.maximalAmoCliques(problem.factors.asList())
 
     /** Duplicate / parallel integer-column aggregation. See [DuplicateColumns]. */
-    fun mergeDuplicateColumns(problem: Problem, objectiveIntVars: Set<Int> = emptySet()): DuplicateColumnMerge =
-        DuplicateColumns.mergeDuplicateColumns(problem, objectiveIntVars)
+    fun mergeDuplicateColumns(
+        problem: Problem,
+        objectiveIntVars: Set<Int> = emptySet(),
+        sharedIntOcc: SharedIntOccurrence? = null,
+    ): PassDelta = DuplicateColumns.mergeDuplicateColumns(problem, objectiveIntVars, sharedIntOcc)
 
     /** Symmetry breaking by detecting interchangeable variables. See [SymmetryBreaking]. */
     fun breakSymmetries(
@@ -48,10 +53,10 @@ object Presolve {
         objectiveIntVars: Set<Int> = emptySet(),
         objectiveBoolVars: Set<Int> = emptySet(),
         cancellation: Cancellation = Cancellation.Never,
-    ): Problem = SymmetryBreaking.breakSymmetries(problem, objectiveIntVars, objectiveBoolVars, cancellation)
+    ): PassDelta = SymmetryBreaking.breakSymmetries(problem, objectiveIntVars, objectiveBoolVars, cancellation)
 
     /** Value-precedence breaking over interchangeable value orbits. See [SymmetryBreaking]. */
-    fun breakValuePrecedence(problem: Problem, objectiveIntVars: Set<Int> = emptySet()): Problem =
+    fun breakValuePrecedence(problem: Problem, objectiveIntVars: Set<Int> = emptySet()): PassDelta =
         SymmetryBreaking.breakValuePrecedence(problem, objectiveIntVars)
 
     /** Dual fixing / dominated-variable reductions. See [DominatedVariables]. */
@@ -59,10 +64,10 @@ object Presolve {
         problem: Problem,
         objectiveIntCoeffs: Map<Int, Long>,
         objectiveBoolCoeffs: Map<Int, Long> = emptyMap(),
-    ): Problem = DominatedVariables.fixDominatedVariables(problem, objectiveIntCoeffs, objectiveBoolCoeffs)
+    ): PassDelta = DominatedVariables.fixDominatedVariables(problem, objectiveIntCoeffs, objectiveBoolCoeffs)
 
     /** Failed-literal and common-bound probing to fixpoint. See [Probing]. */
-    fun probe(problem: Problem, maxCandidates: Int, cancellation: Cancellation = Cancellation.Never): Problem =
+    fun probe(problem: Problem, maxCandidates: Int, cancellation: Cancellation = Cancellation.Never): PassDelta =
         Probing.probe(problem, maxCandidates, cancellation)
 
     /** Binary implication graph: equivalent-literal substitution and transitive reduction. See
@@ -72,7 +77,7 @@ object Presolve {
         maxCandidates: Int,
         cancellation: Cancellation = Cancellation.Never,
         objectiveBoolVars: Set<Int> = emptySet(),
-    ): ImplicationReduction = ImplicationGraph.reduce(problem, maxCandidates, cancellation, objectiveBoolVars)
+    ): PassDelta = ImplicationGraph.reduce(problem, maxCandidates, cancellation, objectiveBoolVars)
 
     /** Binary-implication graph (literal-indexed adjacency `lit -> forced lits`) for implication-aware
      *  consumers such as local search. See [ImplicationGraph]. */
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/PresolveSession.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/PresolveSession.kt
new file mode 100644
index 000000000..7c8c11662
--- /dev/null
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/PresolveSession.kt
@@ -0,0 +1,358 @@
+package com.eignex.klause.presolve
+
+import com.eignex.klause.propagation.PropagationResult
+import com.eignex.klause.propagation.PropagationState
+import com.eignex.klause.solver.Assumptions
+import com.eignex.klause.solver.EmptyIntArray
+import com.eignex.klause.solver.Factor
+import com.eignex.klause.solver.IntDomain
+import com.eignex.klause.solver.Problem
+import com.eignex.klause.util.IntArrayList
+
+/**
+ * A pass's incremental change to the working problem: factors to drop (by stable id), factors to
+ * add, and the pass's directly-derived domain tightenings.
+ *
+ * [domains] carries the pass's own narrowings (a dual-fixed bound, an affine substitution's range) as
+ * a full int-domain array, or `null` when the pass leaves domains alone. Tightenings that follow from
+ * the kept and added factors are re-derived by re-propagation and need not appear here — listing only
+ * what a pass *cannot* have the propagator rediscover keeps the delta minimal and the fixpoint intact.
+ */
+internal class PresolveDelta(
+    val droppedIds: IntArray = EmptyIntArray,
+    val addedFactors: List<Factor> = emptyList(),
+    val domains: Array<IntDomain>? = null,
+) {
+    val isEmpty: Boolean
+        get() = droppedIds.isEmpty() && addedFactors.isEmpty() && domains == null
+}
+
+/**
+ * Int-variable occurrence index over a pass's live factor list, in the [Factor.intVars] CSR layout the
+ * affine / dup-columns candidate searches consume: the factors mentioning var `v` are the dense indices
+ * `flat[offsets(v) until offsets(v + 1)]`, in ascending dense-index order — matching what a fresh
+ * per-pass rebuild over `problem.factors` would produce. [PresolveSession] maintains the underlying
+ * stable-id lists incrementally on each delta and derives this dense view once per firing, so a
+ * non-firing round pays no O(factors) rebuild.
+ */
+class SharedIntOccurrence internal constructor(internal val offsets: IntArray, internal val flat: IntArray)
+
+/**
+ * Owns the persistent state of an incremental presolve run so the round engine never rebuilds a
+ * [Problem] per firing pass. Holds the working factor set as a stable-id, append-only list (a
+ * tombstoned slot becomes `null` and its id is never reused) and one persistent [PropagationState]
+ * sized to the original variable count — valid for the whole run because presolve never renumbers
+ * variables.
+ *
+ * A pass emits a [PresolveDelta]; [apply] drops/adds factors and pushes the pass's domain narrowings
+ * into the live state, then re-propagates incrementally from just that delta via the existing
+ * dirty-variable/watcher machinery. Because the propagators are monotone the greatest fixpoint is
+ * unique, so this reaches the same tightened domains a from-scratch bake over the final factor set
+ * would — no per-pass `computeBaked`. [materialize] builds the heavyweight solver [Problem] once at
+ * the end, with the single renumber/remap.
+ */
+internal class PresolveSession(private val base: Problem, private val bakeConfig: BakeConfig = BakeConfig.NONE) {
+
+    // Working factor set indexed by stable id: `[0, base.factors.size)` are the originals, appended
+    // ids are pass-added factors. `null` marks a tombstoned (dropped) id; ids are never renumbered.
+    // Refilled in place on a [reseed] (a domain-widening pass the incremental path can't express).
+    private val factors: ArrayList<Factor?> = ArrayList<Factor?>(base.factors.size).apply { addAll(base.factors) }
+
+    // The problem the current [state] is baked over: [base] initially, a widening pass's output after a
+    // [reseed]. Its factor count is the stable-id boundary between base and mid-life factors.
+    private var stateProblem: Problem = base
+
+    // Seed the persistent state directly from the base's already-computed root fixpoint
+    // ([Problem.baked], produced once at base construction) rather than re-propagating every factor
+    // inside the presolve window: the seeded pins/bounds are applied through the atom-consistent
+    // mutation API and settle at that same greatest fixpoint. A [PropagationResult.Unsat] base seeds
+    // nothing (the init below adopts its infeasibility).
+    private var state = PropagationState(
+        base,
+        (base.baked as? PropagationResult.Implied)?.toAssumptions() ?: Assumptions.None,
+        incremental = true,
+    )
+
+    /** Set once the base bake or a delta re-propagation derives a root contradiction. */
+    var infeasible: Boolean = false
+        private set
+
+    // Domains as of the last point the problem was still feasible. On infeasibility the reported /
+    // materialized domains are these, not the partially-tightened live ones — mirroring the fresh path,
+    // where `foldIntoDomains` skips on an Unsat bake and the reported span stays at the pre-conflict
+    // domains. Snapshotted at each mutation entry (before its narrowings) and initialised to the base.
+    private var lastFeasibleDomains: Array<IntDomain> = Array(base.numIntVars) { base.intDomains[it] }
+
+    // Stable ids of the live factors [passInput] last returned, parallel to that view's factor list, so
+    // a [PassDelta]'s droppedIndices (into that list) map back to the stable ids [apply] tombstones.
+    private var liveIds: IntArray = IntArray(0)
+
+    // Int-variable occurrence index keyed by stable factor id: `intOcc[v]` holds the stable ids of every
+    // live factor whose [Factor.intVars] contains `v`, in ascending-stable-id (= append) order. Built
+    // once from the base factors and maintained O(delta) in [apply] — an added factor's stable id is
+    // appended to its vars' lists; a tombstoned factor's id stays (filtered on read, its slot is null).
+    // The affine / dup-columns per-round candidate search reads the dense view derived in [passInput],
+    // never rebuilding an occurrence index of its own.
+    private val intOcc: Array<IntArrayList> = Array(base.numIntVars) { IntArrayList(0) }
+
+    // The dense [SharedIntOccurrence] view [passInput] last handed out, and whether the factor set has
+    // changed since it was built. Rebuilt (O(occurrences)) only once per firing; a non-firing stretch of
+    // passes reuses it, so a round that changes nothing pays no occurrence-index rebuild at all.
+    private var occView: SharedIntOccurrence? = null
+    private var occDirty: Boolean = true
+
+    init {
+        for (id in base.factors.indices) recordOccurrences(id, base.factors[id])
+        // The base [Problem] already ran its root bake at construction (outside presolve). If that
+        // proved infeasibility, adopt it directly — re-propagating the whole factor set just to
+        // rediscover a known root conflict is pure waste, and catastrophic on wide domains (a 2M-span
+        // infeasible model spends seconds re-deriving what `base.baked` already holds). Otherwise
+        // establish the fixpoint on the persistent state, priming the watcher/dirty machinery for
+        // incremental re-propagation (the base's folded domains are copied in, so it settles there).
+        if (base.baked is PropagationResult.Unsat) {
+            infeasible = true
+        } else if (state.runToFixpoint(allFactors = false) != null) {
+            infeasible = true
+        }
+    }
+
+    /** Append stable factor id [id] to the occurrence list of each int var factor [f] mentions, so the
+     *  index carries [f] once per occurrence in its [Factor.intVars] (mirroring a fresh CSR rebuild). */
+    private fun recordOccurrences(id: Int, f: Factor) {
+        for (v in f.intVars) intOcc[v].add(id)
+    }
+
+    /** Live (non-tombstoned) factors in stable-id order — the current working constraint set. */
+    fun liveFactors(): List<Factor> = factors.filterNotNull()
+
+    /** Number of live (non-tombstoned) factors. */
+    val liveFactorCount: Int get() = factors.count { it != null }
+
+    /** Cheap problem-complexity measure mirroring [Presolver]'s fresh-path `complexity`: live constraint
+     *  count plus total int-domain span. Drives the round engine's diminishing-returns abort. */
+    fun complexity(): Long {
+        var c = liveFactorCount.toLong()
+        for (v in 0 until base.numIntVars) {
+            val d = state.intDomains[v]
+            c += d.max.toLong() - d.min.toLong()
+        }
+        return c
+    }
+
+    /** The current tightened domain of int var [v] on the persistent state. */
+    fun intDomainOf(v: Int): IntDomain = state.intDomains[v]
+
+    /** Current value of bool var [v] on the persistent state, or `null` if still free. */
+    fun boolValueOf(v: Int): Boolean? = state.boolValues[v]
+
+    /**
+     * Apply [delta] incrementally: tombstone dropped ids, append added factors, push the pass's domain
+     * narrowings, then re-propagate from just the delta. Returns `false` iff this proved infeasibility
+     * (a conflict on a pushed narrowing or during re-propagation); the session latches [infeasible].
+     */
+    fun apply(delta: PresolveDelta): Boolean {
+        if (!infeasible) snapshotFeasibleDomains()
+        if (delta.droppedIds.isNotEmpty() || delta.addedFactors.isNotEmpty()) occDirty = true
+        for (id in delta.droppedIds) {
+            state.tombstoneFactor(id)
+            factors[id] = null
+        }
+        val addedIds = IntArrayList(delta.addedFactors.size)
+        for (f in delta.addedFactors) {
+            val fid = state.addMidlifeFactor(f) // fid == factors.size at this point
+            addedIds.add(fid)
+            factors.add(f)
+            recordOccurrences(fid, f)
+        }
+        // Once infeasible, the factor changes above are still recorded (the materialized problem's bake
+        // resurfaces the infeasibility) but the conflicted state must not be re-propagated. Thread the
+        // pass's output domains forward as the reported domains so a later pass sees this pass's
+        // narrowings — mirroring the fresh path, which carries each pass's fold-skipped domains to the
+        // next, and keeping domain-pinning passes (dual fixing) converging on an infeasible problem.
+        if (infeasible) {
+            delta.domains?.let { d -> lastFeasibleDomains = Array(base.numIntVars) { d[it] } }
+            return false
+        }
+        var ok = pushDomainNarrowings(delta.domains)
+        if (ok && state.runToFixpoint(allFactors = false, initialFactors = addedIds.toIntArray()) != null) ok = false
+        if (!ok) infeasible = true
+        return ok
+    }
+
+    /** Push the per-variable diff of [domains] against the live state into the state's mutation API so
+     *  dependent factors re-wake. `null` (no domain change) is a no-op. Returns false on a conflict. */
+    private fun pushDomainNarrowings(domains: Array<IntDomain>?): Boolean {
+        if (domains == null) return true
+        for (v in domains.indices) {
+            val target = domains[v]
+            val cur = state.intDomains[v]
+            if (target.min == cur.min && target.max == cur.max && target.size == cur.size) continue
+            if (!state.tightenIntMin(v, target.min)) return false
+            if (!state.tightenIntMax(v, target.max)) return false
+            if (!pushInteriorHoles(v, target)) return false
+        }
+        return true
+    }
+
+    /** Remove from int var [v] the interior values the pass carved out of [target] — those still present
+     *  on the state but absent from the target (rare; bound tightenings dominate). Returns false on a
+     *  conflict, and skips the value scan entirely when the state domain already has no extra values. */
+    private fun pushInteriorHoles(v: Int, target: IntDomain): Boolean {
+        if (target.size == state.intDomains[v].size) return true
+        for (value in target.min..target.max) {
+            if (value in target || value !in state.intDomains[v]) continue
+            if (!state.excludeIntValue(v, value)) return false
+        }
+        return true
+    }
+
+    /**
+     * A cheap [Problem] for a pass to read: the live factors and the state's current folded domains,
+     * built in [Problem.preFolded] mode so it never bakes or inverts occurrences. The passes read only
+     * `factors` and `intDomains`, so nothing deferred is ever forced — construction is O(live factors).
+     * Records [liveIds] parallel to the returned factor list so the next [applyDelta] maps the delta's
+     * factor indices back to stable ids.
+     */
+    fun passInput(): Problem {
+        val live = ArrayList<Factor>(factors.size)
+        val ids = IntArrayList(factors.size)
+        for (id in factors.indices) {
+            factors[id]?.let {
+                live.add(it)
+                ids.add(id)
+            }
+        }
+        liveIds = ids.toIntArray()
+        rebuildOccViewIfDirty()
+        return Problem(
+            numBoolVars = base.numBoolVars,
+            numIntVars = base.numIntVars,
+            // Once infeasible, expose the clean pre-conflict domains — not the partially-tightened live ones
+            // a conflicted re-propagation left — so a later pass sees what the fresh path (fold skipped on an
+            // Unsat bake) would and fires identically.
+            intDomains = if (infeasible) lastFeasibleDomains else Array(base.numIntVars) { state.intDomains[it] },
+            factors = live,
+            preFolded = true,
+        )
+    }
+
+    /** The int-variable occurrence index over the factor list [passInput] last returned — the dense CSR
+     *  the affine / dup-columns candidate search would otherwise rebuild itself. Kept in sync with the
+     *  live factors by [passInput]; call it only after [passInput]. */
+    fun passOccurrence(): SharedIntOccurrence = requireNotNull(occView) { "passOccurrence before passInput" }
+
+    /** Derive the dense [SharedIntOccurrence] over the current [liveIds] from the stable-id [intOcc]
+     *  lists, but only when the factor set changed since the last build. Ascending stable id maps to
+     *  ascending dense index (both follow stable-id order), so a var's factors come out in the same
+     *  ascending-dense-index order a fresh `for f in factors for v in f.intVars` CSR would produce —
+     *  byte-identical to the per-pass rebuild the passes drop. Tombstoned ids (dense = -1) are skipped. */
+    private fun rebuildOccViewIfDirty() {
+        if (!occDirty && occView != null) return
+        val denseOf = IntArray(factors.size) { -1 }
+        for (dense in liveIds.indices) denseOf[liveIds[dense]] = dense
+        val offsets = IntArray(base.numIntVars + 1)
+        for (v in 0 until base.numIntVars) {
+            var live = 0
+            val list = intOcc[v]
+            for (k in 0 until list.size) if (denseOf[list[k]] >= 0) live++
+            offsets[v + 1] = offsets[v] + live
+        }
+        val flat = IntArray(offsets[base.numIntVars])
+        val cursor = offsets.copyOf()
+        for (v in 0 until base.numIntVars) {
+            val list = intOcc[v]
+            for (k in 0 until list.size) {
+                val dense = denseOf[list[k]]
+                if (dense >= 0) flat[cursor[v]++] = dense
+            }
+        }
+        occView = SharedIntOccurrence(offsets, flat)
+        occDirty = false
+    }
+
+    /**
+     * Fold a pass's [PassDelta] into the session. Its [PassDelta.droppedIndices] index the factor list
+     * [passInput] last returned, so they are mapped through [liveIds] to stable ids before running the
+     * existing [apply] logic (widen→reseed, infeasible threading, incremental re-propagation). Returns
+     * `false` iff this proved infeasibility.
+     */
+    fun applyDelta(delta: PassDelta): Boolean {
+        val stableDropped = IntArray(delta.droppedIndices.size) { liveIds[delta.droppedIndices[it]] }
+        // A domain *widen* (dup-columns' aggregate variable) can't be reached by monotone re-propagation,
+        // so it triggers a from-scratch reseed — but only while feasible; on an already-infeasible problem
+        // the widen is moot and the factor changes are tracked through [apply].
+        if (!infeasible && delta.domains != null && widensAnyDomain(delta.domains)) {
+            return reseedFromDelta(stableDropped, delta.addedFactors, delta.domains)
+        }
+        return apply(PresolveDelta(stableDropped, delta.addedFactors, delta.domains))
+    }
+
+    /** Whether [domains] widens any variable past the live state — a value the state currently excludes
+     *  becomes allowed. Monotone re-propagation only narrows, so a widen needs a [reseedFromDelta] instead. */
+    private fun widensAnyDomain(domains: Array<IntDomain>): Boolean {
+        for (v in 0 until base.numIntVars) {
+            val cur = state.intDomains[v]
+            val target = domains[v]
+            if (target.min < cur.min || target.max > cur.max || target.size > cur.size) return true
+        }
+        return false
+    }
+
+    /** Rebuild the persistent state from scratch over the delta's output factor set + [domains] (a fresh
+     *  eager bake). Used only when a pass widens a domain; correct because it reproduces the exact
+     *  from-scratch problem for that transition. The output factor set is the live factors minus
+     *  [stableDropped], in stable-id order, followed by [added] — the same set [apply] would land on. */
+    private fun reseedFromDelta(stableDropped: IntArray, added: List<Factor>, domains: Array<IntDomain>): Boolean {
+        val dropped = if (stableDropped.isEmpty()) null else stableDropped.toHashSet()
+        val out = ArrayList<Factor>(factors.size)
+        for (id in factors.indices) {
+            val f = factors[id] ?: continue
+            if (dropped == null || id !in dropped) out.add(f)
+        }
+        out.addAll(added)
+        val eager = PresolveShared.rebuildProblem(base, out, Array(base.numIntVars) { domains[it] }, bakeConfig)
+        stateProblem = eager
+        factors.clear()
+        factors.addAll(eager.factors)
+        // The stable-id space was rebuilt from scratch, so the occurrence lists must be too.
+        for (v in 0 until base.numIntVars) intOcc[v].clear()
+        for (id in eager.factors.indices) recordOccurrences(id, eager.factors[id])
+        occDirty = true
+        state = PropagationState(eager, Assumptions.None, incremental = true)
+        if (state.runToFixpoint(allFactors = true) != null) {
+            infeasible = true
+            return false
+        }
+        return true
+    }
+
+    /** Capture the live domains as the last-feasible snapshot, taken before a mutation's narrowings so
+     *  that if the mutation proves infeasible the reported domains are the pre-conflict ones. */
+    private fun snapshotFeasibleDomains() {
+        lastFeasibleDomains = Array(base.numIntVars) { state.intDomains[it] }
+    }
+
+    /** Materialize the final solver [Problem] once: the live factors and the tightened int domains. On
+     *  infeasibility the pre-conflict [lastFeasibleDomains] are used (the fresh path likewise skips
+     *  folding an Unsat bake); otherwise the state's fully-folded domains.
+     *
+     *  With no root-bake probing enabled (the common incremental case) the state domains are already the
+     *  greatest fixpoint, so the result is [Problem.preFolded]: its `baked` stays lazy and is computed by
+     *  the solver at solve time, not inside the presolve window — the session's own [infeasible] flag
+     *  surfaces the infeasibility to the caller without forcing that bake. When probing *is* enabled it
+     *  must be re-derived over the final factor set (a [RootBaker.reseed] the preFolded view would skip),
+     *  so the eager rebuild path is taken, exactly as before. */
+    fun materialize(): Problem {
+        val domains = if (infeasible) lastFeasibleDomains else Array(base.numIntVars) { state.intDomains[it] }
+        if (bakeConfig.anyEnabled) {
+            return PresolveShared.rebuildProblem(stateProblem, liveFactors(), domains, bakeConfig)
+        }
+        return Problem(
+            numBoolVars = base.numBoolVars,
+            numIntVars = base.numIntVars,
+            intDomains = domains,
+            factors = liveFactors(),
+            preFolded = true,
+        )
+    }
+}
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/PresolveShared.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/PresolveShared.kt
index 77bd1a18c..90923021a 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/PresolveShared.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/PresolveShared.kt
@@ -8,7 +8,9 @@ import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Lit
 import com.eignex.klause.solver.Problem
+import com.eignex.klause.solver.Sample
 import com.eignex.klause.solver.StructuralKey
+import com.eignex.klause.util.IntArrayList
 
 /** Small math and problem-rebuild helpers shared across the presolve passes. */
 internal object PresolveShared {
@@ -118,22 +120,70 @@ internal object PresolveShared {
         return kept
     }
 
+    /**
+     * Materialize the problem that results from applying [delta] to [this] — the fresh-path counterpart
+     * of [PresolveSession.applyDelta]. The next factor list is [this]'s factors with [PassDelta.droppedIndices]
+     * removed (kept in order) followed by [PassDelta.addedFactors]; the domains are the delta's own
+     * ([PassDelta.domains]) or [this]'s when it leaves them alone. Re-baked eagerly through
+     * [rebuildProblem] (the per-firing-pass rebuild the fresh path always did), so it is a plain solver
+     * [Problem] whose `baked` folds the delta's narrowings and any dependent tightenings.
+     */
+    fun Problem.withPassDelta(delta: PassDelta, bakeConfig: BakeConfig): Problem {
+        val kept = ArrayList<Factor>(factors.size - delta.droppedIndices.size + delta.addedFactors.size)
+        val dropped = if (delta.droppedIndices.isEmpty()) null else delta.droppedIndices.toHashSet()
+        for (i in factors.indices) if (dropped == null || i !in dropped) kept.add(factors[i])
+        kept.addAll(delta.addedFactors)
+        return rebuildProblem(this, kept, delta.domains ?: intDomains.copyOf(), bakeConfig)
+    }
+
+    /**
+     * The [PassDelta] taking [inputFactors] to [out] — a rewritten factor list where every survivor is
+     * identity-equal to an input factor ([Factor] uses reference equality, so a plain [HashMap] keys by
+     * identity). Adds every [out] factor absent from the input; drops every input index whose factor is
+     * not among [out]'s survivors. For passes that rebuild their whole factor list (variable renames,
+     * substitutions) rather than deciding keep/drop per input index.
+     */
+    fun identityDelta(
+        inputFactors: Array<Factor>,
+        out: List<Factor>,
+        domains: Array<IntDomain>? = null,
+        reconstruct: ((Sample) -> Sample)? = null,
+    ): PassDelta {
+        val idByFactor = HashMap<Factor, Int>(inputFactors.size)
+        for (i in inputFactors.indices) idByFactor[inputFactors[i]] = i
+        val kept = HashSet<Int>(out.size)
+        val added = ArrayList<Factor>()
+        for (f in out) {
+            val id = idByFactor[f]
+            if (id != null) kept.add(id) else added.add(f)
+        }
+        val dropped = IntArrayList()
+        for (i in inputFactors.indices) if (i !in kept) dropped.add(i)
+        return PassDelta(dropped.toIntArray(), added, domains, reconstruct)
+    }
+
     fun rebuildProblem(
         problem: Problem,
         factors: List<Factor>,
         intDomains: Array<IntDomain> = problem.intDomains.copyOf(),
-    ): Problem = Problem(
-        numBoolVars = problem.numBoolVars,
-        numIntVars = problem.numIntVars,
-        intDomains = intDomains,
-        factors = factors,
-        probeFailedLiterals = problem.probeFailedLiterals,
-        probeIntBounds = problem.probeIntBounds,
-        probeIntHoles = problem.probeIntHoles,
-        probeBudgetPerVar = problem.probeBudgetPerVar,
-        probeTotalBudget = problem.probeTotalBudget,
-        probeSeed = problem.probeSeed,
-    )
+        bakeConfig: BakeConfig = BakeConfig.NONE,
+    ): Problem {
+        // Inherit the pass-view mode: a pass fed a cheap preFolded input returns a cheap preFolded
+        // output (the session re-folds via incremental propagation); a fresh-path rebuild stays eager.
+        val base = Problem(
+            numBoolVars = problem.numBoolVars,
+            numIntVars = problem.numIntVars,
+            intDomains = intDomains,
+            factors = factors,
+            preFolded = problem.preFolded,
+        )
+        // A preFolded pass view never bakes (nothing reads [Problem.baked]), so [RootBaker.reseed] leaves
+        // it untouched; with no probing tier enabled the plain base bake stands. Otherwise the reseed runs
+        // [RootBaker] against the base-baked problem and returns a fresh eager [Problem] whose
+        // [Problem.baked] carries the failed-literal / SAC deductions — the kernel's former self-bake, now
+        // driven from the presolve lane.
+        return RootBaker.reseed(base, bakeConfig)
+    }
 
     fun gcdOf(xs: IntArray): Int {
         var g = 0
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolver.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolver.kt
index 199813170..1378e134b 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolver.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Presolver.kt
@@ -1,6 +1,10 @@
 package com.eignex.klause.presolve
 
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
+import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Cancellation
+import com.eignex.klause.solver.Factor
+import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Problem
 import com.eignex.klause.solver.Sample
 import com.eignex.klause.solver.objective.LinearObjective
@@ -16,6 +20,9 @@ class Presolved(
     /** The problem-stage passes that changed the problem at least once during the run, in first-fire
      *  order — surfaced as presolve statistics (which techniques actually did something). */
     val passesFired: List<PresolvePass> = emptyList(),
+    /** Whether presolve proved the problem infeasible. Surfaced here so the caller need not force the
+     *  materialized [problem]'s lazy `baked` — which the incremental path defers past presolve timing. */
+    val infeasible: Boolean = false,
 )
 
 /**
@@ -44,6 +51,17 @@ class PresolveContext(
      *  partial run only forgoes further reduction, never correctness. [Presolver.run] injects the
      *  round-engine's cancellation here. */
     val cancellation: Cancellation = Cancellation.Never,
+    /** Root-bake probing policy the round engine threads into the materialization of the transformed
+     *  [Problem] — the fresh path's [PresolveShared.withPassDelta] rebuild and the incremental
+     *  [PresolveSession] — so [RootBaker] re-derives the failed-literal / SAC deductions over the final
+     *  factor set. The relocation of the kernel's former `probe*` flags into the presolve lane;
+     *  [BakeConfig.NONE] (the default) leaves the bake a plain base bake. */
+    val bakeConfig: BakeConfig = BakeConfig.NONE,
+    /** The session-maintained int-variable occurrence index over the current pass input, threaded in by
+     *  the incremental round engine so the affine / dup-columns candidate search reads it instead of
+     *  rebuilding an O(factors) index per round. `null` on the fresh path (and outside those passes),
+     *  where each pass falls back to building its own. */
+    val sharedIntOcc: SharedIntOccurrence? = null,
 ) {
     /** Integer variables the objective reads — the nonzero-coefficient indices. */
     val objectiveIntVars: Set<Int> get() = objectiveIntCoeffs.keys
@@ -59,6 +77,32 @@ class PresolveContext(
         objectiveBoolCoeffs,
         modelBreaksSymmetry,
         cancellation,
+        bakeConfig,
+        sharedIntOcc,
+    )
+
+    /** This context with [bakeConfig] set — the presolve lane threads the resolved root-bake probing
+     *  policy in here so every pass rebuild re-derives it via [RootBaker]. */
+    fun withBakeConfig(bakeConfig: BakeConfig): PresolveContext = PresolveContext(
+        solutionSetSensitive,
+        objectiveIntCoeffs,
+        objectiveBoolCoeffs,
+        modelBreaksSymmetry,
+        cancellation,
+        bakeConfig,
+        sharedIntOcc,
+    )
+
+    /** This context carrying the incremental round engine's session-maintained occurrence index for the
+     *  current pass input, so the affine / dup-columns candidate search reuses it. */
+    fun withSharedIntOcc(sharedIntOcc: SharedIntOccurrence?): PresolveContext = PresolveContext(
+        solutionSetSensitive,
+        objectiveIntCoeffs,
+        objectiveBoolCoeffs,
+        modelBreaksSymmetry,
+        cancellation,
+        bakeConfig,
+        sharedIntOcc,
     )
 
     /** Factories for the common contexts. */
@@ -144,10 +188,31 @@ private fun complexity(problem: Problem): Long {
     return c
 }
 
-/** What a [PresolvePass] produced: the (possibly identical) [problem] and, if it changed the
- *  variable mapping, the [reconstruct] that lifts a solution back. `problem === input` signals the
- *  pass was a no-op this round (the engine uses identity to detect the fixpoint). */
-class PassResult(val problem: Problem, val reconstruct: ((Sample) -> Sample)? = null)
+/**
+ * A pass's explicit change to the problem it was given: [droppedIndices] into the input's factor list
+ * (factors removed or replaced), [addedFactors] to append (brand-new or rewritten factors), and
+ * [domains] the pass's directly-derived tightened int domains (or `null` when it leaves domains alone).
+ * A factor rewrite is a drop of its index plus an add of the replacement; a no-op pass returns an
+ * empty [PassDelta] ([isEmpty]), which the round engine treats as the fixpoint signal. [reconstruct]
+ * lifts a solution of the transformed problem back when the pass changed the variable mapping.
+ *
+ * The round engine materializes the next problem from the delta (fresh path) or folds it into the
+ * persistent [PresolveSession] (incremental path); neither rebuilds a whole [Problem] inside the pass.
+ */
+class PassDelta(
+    /** Indices into the input [Problem.factors] that were removed or replaced. */
+    val droppedIndices: IntArray = IntArray(0),
+    /** Brand-new or rewritten factors to append after the kept ones. */
+    val addedFactors: List<Factor> = emptyList(),
+    /** The pass's directly-derived tightened int domains, or `null` when it leaves domains alone. */
+    val domains: Array<IntDomain>? = null,
+    /** Lifts a solution of the transformed problem back to the pass's input, when the pass changed the
+     *  variable mapping (affine / dup-columns / implication merges); `null` for a plain transform. */
+    val reconstruct: ((Sample) -> Sample)? = null,
+) {
+    /** Whether the pass changed nothing this round — the round engine's fixpoint signal. */
+    val isEmpty: Boolean get() = droppedIndices.isEmpty() && addedFactors.isEmpty() && domains == null
+}
 
 /**
  * The catalogue of presolve passes. Each entry co-locates its metadata with [apply], so adding or
@@ -183,8 +248,7 @@ enum class PresolvePass(
 ) {
     /** GCD + bounded-integer coefficient strengthening (#319 / #372). */
     STRENGTHEN_COEFFICIENTS("strengthen", Stage.PROBLEM, PresolveTiming.FAST, true, autoEligible = true) {
-        override fun apply(problem: Problem, ctx: PresolveContext) =
-            PassResult(Presolve.strengthenCoefficients(problem))
+        override fun apply(problem: Problem, ctx: PresolveContext) = Presolve.strengthenCoefficients(problem)
     },
 
     /** One-shot GF(2) elimination over all xor factors: emit implied root unit clauses. */
@@ -196,7 +260,7 @@ enum class PresolvePass(
         autoEligible = true,
         skipAfterEmpty = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext) = PassResult(Presolve.deriveXorUnits(problem))
+        override fun apply(problem: Problem, ctx: PresolveContext) = Presolve.deriveXorUnits(problem)
     },
 
     /** Affine singleton elimination (#318) — reconstructs the eliminated variable. The eliminated
@@ -211,18 +275,15 @@ enum class PresolvePass(
         preservesSolutionSet = false,
         autoEligible = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext): PassResult {
-            val elim = Presolve.eliminateAffineSingletons(problem, ctx.objectiveIntVars, ctx.cancellation)
-            return PassResult(elim.problem, elim::reconstruct)
-        }
+        override fun apply(problem: Problem, ctx: PresolveContext) =
+            Presolve.eliminateAffineSingletons(problem, ctx.objectiveIntVars, ctx.cancellation, ctx.sharedIntOcc)
     },
 
     /** Constraint subsumption / redundant-constraint removal (#447) — drops duplicate factors and
      *  dominated linear inequalities. Runs after the simplifying passes so proportional rows are
      *  already GCD-normalised. */
     REMOVE_REDUNDANT("subsume", Stage.PROBLEM, PresolveTiming.FAST, true, autoEligible = true) {
-        override fun apply(problem: Problem, ctx: PresolveContext) =
-            PassResult(Presolve.removeRedundantConstraints(problem))
+        override fun apply(problem: Problem, ctx: PresolveContext) = Presolve.removeRedundantConstraints(problem)
     },
 
     /** Per-factor structural self-reduction — each factor rewrites itself into simpler / lower-arity
@@ -235,7 +296,7 @@ enum class PresolvePass(
         preservesSolutionSet = true,
         autoEligible = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext) = PassResult(Presolve.reduceStructural(problem))
+        override fun apply(problem: Problem, ctx: PresolveContext) = Presolve.reduceStructural(problem)
     },
 
     /** Duplicate / parallel column aggregation — the column-side mirror of [REMOVE_REDUNDANT]. Folds
@@ -250,10 +311,8 @@ enum class PresolvePass(
         preservesSolutionSet = false,
         autoEligible = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext): PassResult {
-            val merge = Presolve.mergeDuplicateColumns(problem, ctx.objectiveIntVars)
-            return PassResult(merge.problem, merge::reconstruct)
-        }
+        override fun apply(problem: Problem, ctx: PresolveContext) =
+            Presolve.mergeDuplicateColumns(problem, ctx.objectiveIntVars, ctx.sharedIntOcc)
     },
 
     /** Interchangeable-variable / block / value symmetry breaking (#317 / #367 / #373 / #366). */
@@ -265,8 +324,12 @@ enum class PresolvePass(
         autoEligible = true,
         skipAfterEmpty = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext) =
-            PassResult(Presolve.breakSymmetries(problem, ctx.objectiveIntVars, ctx.objectiveBoolVars, ctx.cancellation))
+        override fun apply(problem: Problem, ctx: PresolveContext) = Presolve.breakSymmetries(
+            problem,
+            ctx.objectiveIntVars,
+            ctx.objectiveBoolVars,
+            ctx.cancellation,
+        )
     },
 
     /** Law–Lee value precedence (#374 / #432) — the strong value-symmetry break. Opt-in: stacking it
@@ -280,7 +343,7 @@ enum class PresolvePass(
         autoEligible = false,
     ) {
         override fun apply(problem: Problem, ctx: PresolveContext) =
-            PassResult(Presolve.breakValuePrecedence(problem, ctx.objectiveIntVars))
+            Presolve.breakValuePrecedence(problem, ctx.objectiveIntVars)
     },
 
     /** Dual fixing / dominated-variable reductions (#448) — pins a variable to a bound when the
@@ -288,7 +351,7 @@ enum class PresolvePass(
      *  auto-disabled for solution-set-sensitive queries. */
     DUAL_FIX("dual-fix", Stage.PROBLEM, PresolveTiming.MEDIUM, preservesSolutionSet = false, autoEligible = true) {
         override fun apply(problem: Problem, ctx: PresolveContext) =
-            PassResult(Presolve.fixDominatedVariables(problem, ctx.objectiveIntCoeffs, ctx.objectiveBoolCoeffs))
+            Presolve.fixDominatedVariables(problem, ctx.objectiveIntCoeffs, ctx.objectiveBoolCoeffs)
     },
 
     /** Construction-time failed-literal SAC (#146): folded into `Problem.baked` at build, read via
@@ -300,17 +363,17 @@ enum class PresolvePass(
         true,
         autoEligible = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext) = PassResult(problem)
+        override fun apply(problem: Problem, ctx: PresolveContext) = PassDelta()
     },
 
     /** Construction-time bound SAC. */
     PROBE_INT_BOUNDS("probe-int-bounds", Stage.CONSTRUCTION, PresolveTiming.EXHAUSTIVE, true, autoEligible = true) {
-        override fun apply(problem: Problem, ctx: PresolveContext) = PassResult(problem)
+        override fun apply(problem: Problem, ctx: PresolveContext) = PassDelta()
     },
 
     /** Construction-time interior-hole SAC; implies [PROBE_INT_BOUNDS]. */
     PROBE_INT_HOLES("probe-int-holes", Stage.CONSTRUCTION, PresolveTiming.EXHAUSTIVE, true, autoEligible = true) {
-        override fun apply(problem: Problem, ctx: PresolveContext) = PassResult(problem)
+        override fun apply(problem: Problem, ctx: PresolveContext) = PassDelta()
     },
 
     /** Probing to fixpoint: tentatively pin each free Boolean, propagate, and keep only the
@@ -318,7 +381,7 @@ enum class PresolvePass(
      *  common-bound tightenings. Solution-preserving, so it needs no objective-variable exclusion. */
     PROBE("probe", Stage.PROBLEM, PresolveTiming.EXHAUSTIVE, true, autoEligible = true) {
         override fun apply(problem: Problem, ctx: PresolveContext) =
-            PassResult(Presolve.probe(problem, PROBE_PASS_MAX_CANDIDATES, Cancellation.Never))
+            Presolve.probe(problem, PROBE_PASS_MAX_CANDIDATES, Cancellation.Never)
     },
 
     /** Binary implication graph: harvest `lit -> lit` implications by probing-style pinning, collapse
@@ -333,15 +396,12 @@ enum class PresolvePass(
         preservesSolutionSet = false,
         autoEligible = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext): PassResult {
-            val reduction = Presolve.reduceImplicationGraph(
-                problem,
-                IMPLICATION_GRAPH_MAX_CANDIDATES,
-                Cancellation.Never,
-                ctx.objectiveBoolVars,
-            )
-            return PassResult(reduction.problem, reduction::reconstruct)
-        }
+        override fun apply(problem: Problem, ctx: PresolveContext) = Presolve.reduceImplicationGraph(
+            problem,
+            IMPLICATION_GRAPH_MAX_CANDIDATES,
+            Cancellation.Never,
+            ctx.objectiveBoolVars,
+        )
     },
 
     /** LP-relaxation harvest: fold the LP's proven domain tightenings, redundant-row removals, root
@@ -359,13 +419,13 @@ enum class PresolvePass(
         preservesSolutionSet = true,
         autoEligible = true,
     ) {
-        override fun apply(problem: Problem, ctx: PresolveContext) = PassResult(problem)
+        override fun apply(problem: Problem, ctx: PresolveContext) = PassDelta()
     },
     ;
 
-    /** Transform [problem] under [ctx]. The returned [PassResult.problem] is `=== problem` when the
-     *  pass found nothing to do this round. */
-    abstract fun apply(problem: Problem, ctx: PresolveContext): PassResult
+    /** Transform [problem] under [ctx], returning the change as a [PassDelta] against [problem]'s factor
+     *  list. An empty delta ([PassDelta.isEmpty]) signals the pass found nothing to do this round. */
+    abstract fun apply(problem: Problem, ctx: PresolveContext): PassDelta
 
     /** Where a pass runs. */
     enum class Stage {
@@ -595,6 +655,13 @@ object Presolver {
         // between passes.
         val ctx = context.withCancellation(cancellation)
 
+        // Incremental path for the default FAST+MEDIUM rounds: one persistent [PresolveSession] absorbs
+        // each pass's delta instead of rebuilding a [Problem] per firing pass. Scoped away from any
+        // EXHAUSTIVE (SAC / LP-harvest) pass, whose order-sensitive probing keeps the fresh-rebuild path.
+        if (passes.none { it.timing == PresolveTiming.EXHAUSTIVE }) {
+            return runIncremental(problem, passes, maxRounds, ctx, cancellation)
+        }
+
         var current = problem
         val reconstructs = ArrayList<(Sample) -> Sample>() // in application order
         // A monotone "problem version" bumped on every change; a pass that already ran at the current
@@ -616,11 +683,10 @@ object Presolver {
                 if (ranAtVersion[pass] == version) continue
                 ranAtVersion[pass] = version
                 ranAny = true
-                val before = current
-                val result = pass.apply(current, ctx)
-                if (result.problem !== before) {
-                    current = result.problem
-                    result.reconstruct?.let { reconstructs.add(it) }
+                val delta = pass.apply(current, ctx)
+                if (!delta.isEmpty) {
+                    current = current.withPassDelta(delta, ctx.bakeConfig)
+                    delta.reconstruct?.let { reconstructs.add(it) }
                     fired.add(pass)
                     version++
                 } else if (pass.skipAfterEmpty) {
@@ -645,6 +711,77 @@ object Presolver {
             } else {
                 { sample -> reconstructs.foldRight(sample) { f, acc -> f(acc) } }
             }
-        return Presolved(current, reconstruct, fired.toList())
+        return Presolved(current, reconstruct, fired.toList(), current.baked is PropagationResult.Unsat)
+    }
+
+    /**
+     * Incremental variant of [run]'s round engine (default FAST+MEDIUM emphasis): identical
+     * scheduling — priority order, version-stamp fixpoint skip, [PresolvePass.skipAfterEmpty] parking,
+     * and the diminishing-returns abort — but a persistent [PresolveSession] absorbs each firing pass's
+     * delta instead of rebuilding a [Problem]. Each pass reads a cheap [PresolveSession.passInput] view
+     * and its delta is folded back via [PresolveSession.applyDelta]; the heavyweight solver [Problem]
+     * is materialized once at the end.
+     */
+    private fun runIncremental(
+        problem: Problem,
+        passes: List<PresolvePass>,
+        maxRounds: Int,
+        ctx: PresolveContext,
+        cancellation: Cancellation,
+    ): Presolved {
+        val session = PresolveSession(problem, ctx.bakeConfig)
+        val reconstructs = ArrayList<(Sample) -> Sample>()
+        var version = 0
+        val ranAtVersion = HashMap<PresolvePass, Int>()
+        val fired = LinkedHashSet<PresolvePass>()
+        val exhausted = HashSet<PresolvePass>()
+        var round = 0
+        var roundStartComplexity = session.complexity()
+        // Infeasibility does not stop the loop, mirroring the fresh path: a pass still fires and records
+        // its factors on an already-infeasible problem (e.g. xor-units emitting contradictory units).
+        // [PresolveSession.applyDelta] tracks those factor changes but skips re-propagating a conflicted
+        // state, and the final materialized problem's bake surfaces the infeasibility.
+        while (round < maxRounds && !cancellation()) {
+            var ranAny = false
+            for (pass in passes) {
+                if (cancellation()) break
+                if (pass in exhausted) continue
+                if (ranAtVersion[pass] == version) continue
+                ranAtVersion[pass] = version
+                ranAny = true
+                val input = session.passInput()
+                // Hand the session's incrementally-maintained occurrence index to the pass so the affine
+                // / dup-columns candidate search reads it instead of rebuilding an O(factors) index; the
+                // view matches [input]'s factor order exactly, so decisions are unchanged.
+                val delta = pass.apply(input, ctx.withSharedIntOcc(session.passOccurrence()))
+                if (!delta.isEmpty) {
+                    delta.reconstruct?.let { reconstructs.add(it) }
+                    session.applyDelta(delta)
+                    fired.add(pass)
+                    version++
+                } else if (pass.skipAfterEmpty) {
+                    exhausted.add(pass)
+                }
+            }
+            if (!ranAny) break
+            round++
+            val now = session.complexity()
+            val reduced = roundStartComplexity - now
+            if (reduced > 0 && reduced.toDouble() < PRESOLVE_ABORT_FRACTION * roundStartComplexity) break
+            roundStartComplexity = now
+        }
+
+        // No pass fired: presolve is a no-op, so return the input problem itself (identity) exactly like
+        // the fresh path returns `current === problem` — several callers assertSame on a fixpoint.
+        if (fired.isEmpty()) return Presolved(problem, { it }, emptyList())
+
+        val finalProblem = session.materialize()
+        val reconstruct: (Sample) -> Sample =
+            if (reconstructs.isEmpty()) {
+                { it }
+            } else {
+                { sample -> reconstructs.foldRight(sample) { f, acc -> f(acc) } }
+            }
+        return Presolved(finalProblem, reconstruct, fired.toList(), session.infeasible)
     }
 }
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Probing.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Probing.kt
index b03436339..e527cabe1 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Probing.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/Probing.kt
@@ -34,7 +34,7 @@ internal object Probing {
      * Booleans cannot blow up presolve time; the round engine re-enters the pass after other passes
      * fire, and a later round picks up where bumping units shifted the free set.
      */
-    fun probe(problem: Problem, maxCandidates: Int, cancellation: Cancellation): Problem {
+    fun probe(problem: Problem, maxCandidates: Int, cancellation: Cancellation): PassDelta {
         val pinned = IntHashSet()
         for (f in problem.factors) {
             if (f is Clause && f.literals.size == 1) pinned.add(Lit.variable(f.literals[0]))
@@ -73,9 +73,8 @@ internal object Probing {
             v++
         }
 
-        if (units.isEmpty() && !domainsChanged) return problem
-        val factors = if (units.isEmpty()) problem.factors.toList() else problem.factors.toList() + units
-        return PresolveShared.rebuildProblem(problem, factors, domains)
+        if (units.isEmpty() && !domainsChanged) return PassDelta()
+        return PassDelta(addedFactors = units, domains = if (domainsChanged) domains else null)
     }
 
     /** Fold the intersection of the bounds implied under each polarity into [domains]; return whether
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/RedundantConstraints.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/RedundantConstraints.kt
index d8f096ddb..ad7b27ca7 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/RedundantConstraints.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/RedundantConstraints.kt
@@ -12,6 +12,7 @@ import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Problem
 import com.eignex.klause.solver.StructuralKey
+import com.eignex.klause.util.IntArrayList
 import com.eignex.klause.util.IntHashSet
 import com.eignex.klause.util.MutableIntIntMap
 import com.eignex.kumulant.math.splitmix64
@@ -44,7 +45,7 @@ internal object RedundantConstraints {
      * (maximal activity already within the bound) are dropped by the strengthen lift, so this pass is
      * purely cross-constraint.
      */
-    fun removeRedundantConstraints(problem: Problem): Problem {
+    fun removeRedundantConstraints(problem: Problem): PassDelta {
         val factors = problem.factors
         // Phase 1: exact-duplicate removal by structural key, two-tier so the full key — which for a
         // Table embeds its entire sorted tuple set and dominates presolve time on table-heavy models —
@@ -129,8 +130,16 @@ internal object RedundantConstraints {
         // Phase 5: drop globals the current domains make vacuously satisfied (#553); removing one frees
         // a variable contained only in it, which the affine pass then projects out (implied-free).
         val out5 = out4.filterNot { isVacuousGlobal(it, problem.intDomains) }
-        if (out5.size == factors.size) return problem
-        return PresolveShared.rebuildProblem(problem, out5)
+        if (out5.size == factors.size) return PassDelta()
+        // This pass only drops; every survivor in [out5] is identity-equal to an input factor, in input
+        // order, so a two-pointer walk recovers the dropped input indices (correct even with reference
+        // duplicates, which Phase 1 collapses to one survivor).
+        val dropped = IntArrayList(factors.size - out5.size)
+        var p = 0
+        for (i in factors.indices) {
+            if (p < out5.size && factors[i] === out5[p]) p++ else dropped.add(i)
+        }
+        return PassDelta(dropped.toIntArray())
     }
 
     /** Whether [factor] is a global constraint that the current [domains] make *vacuously* satisfied —
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/RootBaker.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/RootBaker.kt
new file mode 100644
index 000000000..8b89c9521
--- /dev/null
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/RootBaker.kt
@@ -0,0 +1,287 @@
+package com.eignex.klause.presolve
+
+import com.eignex.klause.propagation.PropagationResult
+import com.eignex.klause.solver.Assumptions
+import com.eignex.klause.solver.Problem
+import kotlin.random.Random
+
+/**
+ * Bake-time root probing, moved out of the kernel [Problem] into the presolve lane.
+ *
+ * A [Problem] only ever performs the cheap unconditional *base bake* (one `propagate(Assumptions.None)`
+ * folded into its domains). The heavier failed-literal / SAC probing tiers — which are only ever enabled
+ * by the compile / presolve layers — live here so the kernel never depends on `presolve` (the
+ * `solver → presolve → solver` cycle the package split exists to prevent).
+ *
+ * [bake] runs the probing fixpoint against an already-base-baked [Problem] (probing calls
+ * `problem.propagate(assumptions)` exactly as the kernel used to) and returns the accumulated
+ * deductions. The pipeline feeds that back as [Problem]'s `seedDeductions`, so the rebuilt problem's
+ * [Problem.baked] carries the probing pins / bound tightenings / holes.
+ */
+object RootBaker {
+
+    /**
+     * Re-seed a base-baked [problem] with the [config]-enabled probing tiers: run [bake] and, when it
+     * found extra deductions, return a fresh eager [Problem] over the same factors / domains whose
+     * [Problem.baked] carries them. Returns [problem] unchanged when no tier is enabled, the problem is
+     * a [Problem.preFolded] pass view (which never bakes), or the base bake is already `Unsat`. This is
+     * the central re-probe point for the presolve fresh path and the LP harvest — the kernel never
+     * initiates it, so no `solver → presolve` cycle.
+     */
+    fun reseed(problem: Problem, config: BakeConfig): Problem {
+        if (!config.anyEnabled || problem.preFolded) return problem
+        val extra = bake(problem, config)
+        if (extra === problem.baked) return problem
+        return Problem(
+            numBoolVars = problem.numBoolVars,
+            numIntVars = problem.numIntVars,
+            intDomains = Array(problem.numIntVars) { problem.intDomains[it] },
+            factors = problem.factors,
+            seedDeductions = extra,
+            cancellation = problem.cancellation,
+            impliedFactorMask = problem.impliedFactorMask,
+            hasSymmetryBreaking = problem.hasSymmetryBreaking,
+        )
+    }
+
+    /**
+     * Run the [config]-enabled probing tiers against the base-baked [problem] and return the resulting
+     * deductions — the base bake merged with every probing finding, ready to seed a rebuilt [Problem].
+     * Returns [problem]'s existing bake unchanged when no tier is enabled or the base bake is already
+     * `Unsat`. Cancellation is polled between phases and probes; a fired deadline yields a sound partial
+     * bake (probing only ever tightens).
+     */
+    fun bake(problem: Problem, config: BakeConfig): PropagationResult {
+        val base = problem.baked
+        if (base !is PropagationResult.Implied) return base
+        if (!config.anyEnabled) return base
+        // SAC probing fires `propagate` repeatedly; stop entering new probe phases once the bake
+        // deadline has passed (each phase below also polls between its own probes).
+        if (problem.cancellation()) return base
+        var result: PropagationResult = base
+        if (config.probeFailedLiterals) {
+            result = probeFreeBools(problem, base)
+            if (result is PropagationResult.Unsat) return result
+        }
+        if (config.probeIntBounds || config.probeIntHoles) {
+            // wdeg state shared across bound-SAC and hole-SAC: a probe failure under bound-SAC raises
+            // factor weights that then steer hole-SAC's first iteration, and vice versa.
+            val factorWeights = DoubleArray(problem.numFactors) { 1.0 }
+            val rng = Random(config.probeSeed)
+            result = probeBoundSac(problem, result as PropagationResult.Implied, config, factorWeights, rng)
+            if (result is PropagationResult.Unsat) return result
+            if (config.probeIntHoles) {
+                result = probeIntHoles(problem, result as PropagationResult.Implied, config, factorWeights, rng)
+            }
+        }
+        return result
+    }
+
+    /** Interior-value SAC: probe every value strictly between each multi-value int var's current min
+     *  and max. Iterates with bound-SAC interleaved so hole-discovered tightenings can lift bounds and
+     *  vice versa. */
+    private fun probeIntHoles(
+        problem: Problem,
+        base: PropagationResult.Implied,
+        config: BakeConfig,
+        factorWeights: DoubleArray,
+        rng: Random,
+    ): PropagationResult {
+        var acc: PropagationResult.Implied = base
+        val perVarCalls = IntArray(problem.numIntVars)
+        var totalCalls = 0
+        var changed = true
+        while (changed) {
+            changed = false
+            for (v in sacProbeOrder(problem, acc, factorWeights, rng)) {
+                if (problem.cancellation()) return acc
+                if (acc.intValueOrNull(v) != null) continue
+                if (perVarCalls[v] >= config.probeBudgetPerVar) continue
+                if (totalCalls >= config.probeTotalBudget) return acc
+                val orig = problem.intDomains[v]
+                val curMin = acc.intMinOrNullCompat(v) ?: orig.min
+                val curMax = acc.intMaxOrNullCompat(v) ?: orig.max
+                if (curMin >= curMax) continue
+                val accAsAssumptions = acc.toAssumptions()
+                // Build a per-var hole-set once so the `alreadyHole` lookup in the k-loop is O(1)
+                // instead of a linear scan of acc.intHoleVarIds for every probed k.
+                val existingHoles = HashSet<Int>()
+                for (i in 0 until acc.intHoleVarIds.size) {
+                    if (acc.intHoleVarIds[i] == v) existingHoles.add(acc.intHoleValues[i])
+                }
+                for (k in (curMin + 1) until curMax) {
+                    if (perVarCalls[v] >= config.probeBudgetPerVar) break
+                    if (totalCalls >= config.probeTotalBudget) return acc
+                    if (k !in orig) continue
+                    if (k in existingHoles) continue
+                    perVarCalls[v]++
+                    totalCalls++
+                    val pin = problem.propagate(accAsAssumptions.withInt(v, k), problem.cancellation)
+                    if (pin is PropagationResult.Unsat) {
+                        bumpFactorWeights(pin, factorWeights)
+                        perVarCalls[v]++
+                        totalCalls++
+                        val r = problem.propagate(accAsAssumptions.withIntHole(v, k), problem.cancellation)
+                        if (r is PropagationResult.Unsat) return r
+                        acc = acc.withHole(v, k).merge(r as PropagationResult.Implied)
+                        changed = true
+                    }
+                }
+            }
+        }
+        return acc
+    }
+
+    /** Probe-order heuristic: wdeg / dom — sort descending by `Σ factorWeights(f) / dom(v)` so the
+     *  budget is spent first on vars that are heavily-constrained relative to their remaining domain.
+     *  Each Unsat probe bumps the weights of the factors in its conflict via [bumpFactorWeights], so
+     *  failing probes steer the next pass toward related vars (the classic wdeg adaptation). Ties break
+     *  by a per-pass random key (deterministic for a given seed) — this avoids the deterministic-id-order
+     *  bias the prior dom-sized order would inherit when every var has the same dom and weight. */
+    private fun sacProbeOrder(
+        problem: Problem,
+        acc: PropagationResult.Implied,
+        factorWeights: DoubleArray,
+        rng: Random,
+    ): IntArray {
+        val numIntVars = problem.numIntVars
+        val scores = DoubleArray(numIntVars) { v ->
+            if (acc.intValueOrNull(v) != null) return@DoubleArray Double.NEGATIVE_INFINITY
+            val orig = problem.intDomains[v]
+            val lo = acc.intMinOrNullCompat(v) ?: orig.min
+            val hi = acc.intMaxOrNullCompat(v) ?: orig.max
+            val dom = (hi - lo + 1).coerceAtLeast(1)
+            var wdeg = 0.0
+            val occ = problem.intOccurrences[v]
+            for (i in occ.indices) wdeg += factorWeights[occ[i]]
+            wdeg / dom
+        }
+        val tie = IntArray(numIntVars) { rng.nextInt() }
+        val boxed = Array(numIntVars) { it }
+        boxed.sortWith(
+            Comparator { a, b ->
+                val sa = scores[a]
+                val sb = scores[b]
+                if (sa != sb) sb.compareTo(sa) else tie[a].compareTo(tie[b])
+            },
+        )
+        return IntArray(numIntVars) { boxed[it] }
+    }
+
+    /** Bump every factor implicated in an Unsat conflict by 1.0. This is the wdeg update rule: factors
+     *  that repeatedly fail under hypothetical pins gain weight and steer the SAC probe order toward the
+     *  vars they mention on subsequent passes. */
+    private fun bumpFactorWeights(unsat: PropagationResult.Unsat, factorWeights: DoubleArray) {
+        for (f in unsat.conflictFactors) {
+            if (f in factorWeights.indices) factorWeights[f] += 1.0
+        }
+    }
+
+    /**
+     * Bound-SAC fixed-point loop. Probes the min and max of each multi-value int var under the current
+     * [base]; an Unsat result lets us tighten that bound by one and re-probe. Returns the strengthened
+     * [PropagationResult.Implied], or `Unsat` if the problem turns out to be infeasible.
+     */
+    private fun probeBoundSac(
+        problem: Problem,
+        base: PropagationResult.Implied,
+        config: BakeConfig,
+        factorWeights: DoubleArray,
+        rng: Random,
+    ): PropagationResult {
+        var acc: PropagationResult.Implied = base
+        val perVarCalls = IntArray(problem.numIntVars)
+        var totalCalls = 0
+        var changed = true
+        while (changed) {
+            changed = false
+            for (v in sacProbeOrder(problem, acc, factorWeights, rng)) {
+                if (problem.cancellation()) return acc
+                if (acc.intValueOrNull(v) != null) continue
+                if (perVarCalls[v] >= config.probeBudgetPerVar) continue
+                if (totalCalls >= config.probeTotalBudget) return acc
+                val orig = problem.intDomains[v]
+                val curMin = acc.intMinOrNullCompat(v) ?: orig.min
+                val curMax = acc.intMaxOrNullCompat(v) ?: orig.max
+                if (curMin >= curMax) continue
+                val accAsAssumptions = acc.toAssumptions()
+                perVarCalls[v]++
+                totalCalls++
+                val pinMin = problem.propagate(accAsAssumptions.withInt(v, curMin), problem.cancellation)
+                if (pinMin is PropagationResult.Unsat) {
+                    bumpFactorWeights(pinMin, factorWeights)
+                    perVarCalls[v]++
+                    totalCalls++
+                    val tightened = accAsAssumptions.withTightenedMin(v, curMin + 1)
+                    val r = problem.propagate(tightened, problem.cancellation)
+                    if (r is PropagationResult.Unsat) return r
+                    acc = acc.withMin(v, curMin + 1).merge(r as PropagationResult.Implied)
+                    changed = true
+                    continue
+                }
+                if (perVarCalls[v] >= config.probeBudgetPerVar) continue
+                if (totalCalls >= config.probeTotalBudget) return acc
+                perVarCalls[v]++
+                totalCalls++
+                val pinMax = problem.propagate(accAsAssumptions.withInt(v, curMax), problem.cancellation)
+                if (pinMax is PropagationResult.Unsat) {
+                    bumpFactorWeights(pinMax, factorWeights)
+                    perVarCalls[v]++
+                    totalCalls++
+                    val tightened = accAsAssumptions.withTightenedMax(v, curMax - 1)
+                    val r = problem.propagate(tightened, problem.cancellation)
+                    if (r is PropagationResult.Unsat) return r
+                    acc = acc.withMax(v, curMax - 1).merge(r as PropagationResult.Implied)
+                    changed = true
+                }
+            }
+        }
+        return acc
+    }
+
+    /**
+     * Iteratively strengthens [initial] by probing each free bool with both polarities. If one polarity
+     * is Unsat under the current accumulated base, the opposite polarity is forced. Repeats until a full
+     * pass finds no new forcings.
+     */
+    private fun probeFreeBools(problem: Problem, initial: PropagationResult.Implied): PropagationResult {
+        val bools = HashMap(initial.bools)
+        val ints = HashMap(initial.ints)
+        var changed = true
+        while (changed) {
+            changed = false
+            for (v in 0 until problem.numBoolVars) {
+                if (problem.cancellation()) return PropagationResult.Implied(bools, ints)
+                if (v in bools) continue
+                val tryTrue = problem.propagate(Assumptions(bools + (v to true), ints), problem.cancellation)
+                if (tryTrue is PropagationResult.Unsat) {
+                    val r = problem.propagate(Assumptions(bools + (v to false), ints), problem.cancellation)
+                    if (r is PropagationResult.Unsat) return r
+                    foldInto(bools, ints, v, false, r as PropagationResult.Implied)
+                    changed = true
+                    continue
+                }
+                val tryFalse = problem.propagate(Assumptions(bools + (v to false), ints), problem.cancellation)
+                if (tryFalse is PropagationResult.Unsat) {
+                    val r = problem.propagate(Assumptions(bools + (v to true), ints), problem.cancellation)
+                    if (r is PropagationResult.Unsat) return r
+                    foldInto(bools, ints, v, true, r as PropagationResult.Implied)
+                    changed = true
+                }
+            }
+        }
+        return PropagationResult.Implied(bools, ints)
+    }
+
+    private fun foldInto(
+        bools: HashMap<Int, Boolean>,
+        ints: HashMap<Int, Int>,
+        forcedVar: Int,
+        forcedValue: Boolean,
+        implied: PropagationResult.Implied,
+    ) {
+        bools[forcedVar] = forcedValue
+        implied.forEachBool { k, b -> bools[k] = b }
+        implied.forEachInt { k, i -> ints[k] = i }
+    }
+}
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/StructuralReduction.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/StructuralReduction.kt
index 08c3f0304..bec9a3156 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/StructuralReduction.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/StructuralReduction.kt
@@ -4,6 +4,7 @@ import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.FactorReduction
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Problem
+import com.eignex.klause.util.IntArrayList
 
 internal object StructuralReduction {
 
@@ -13,17 +14,17 @@ internal object StructuralReduction {
      * solution-set exact (the hook's contract), so the pass preserves the solution set; the driver only
      * collects the replacements, intersects any returned bound narrowings into the domains, and rebuilds.
      */
-    fun reduce(problem: Problem): Problem {
-        var changed = false
+    fun reduce(problem: Problem): PassDelta {
+        val dropped = IntArrayList()
+        val added = ArrayList<Factor>()
         var domains: Array<IntDomain>? = null
-        val out = ArrayList<Factor>(problem.factors.size)
-        for (f in problem.factors) {
+        problem.factors.forEachIndexed { i, f ->
             when (val reduction = f.structuralReduce(problem.intDomains)) {
-                FactorReduction.Unchanged -> out.add(f)
+                FactorReduction.Unchanged -> {}
 
                 is FactorReduction.Rewrite -> {
-                    changed = true
-                    out.addAll(reduction.replacement)
+                    dropped.add(i)
+                    added.addAll(reduction.replacement)
                     for ((v, range) in reduction.tightenedBounds) {
                         val d = domains ?: problem.intDomains.copyOf().also { domains = it }
                         d[v] = d[v].withMinAtLeast(range.first).withMaxAtMost(range.last)
@@ -31,7 +32,7 @@ internal object StructuralReduction {
                 }
             }
         }
-        if (!changed) return problem
-        return PresolveShared.rebuildProblem(problem, out, domains ?: problem.intDomains.copyOf())
+        if (dropped.isEmpty()) return PassDelta()
+        return PassDelta(dropped.toIntArray(), added, domains)
     }
 }
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/SymmetryBreaking.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/SymmetryBreaking.kt
index 9eff525c4..77f0ae71a 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/SymmetryBreaking.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/SymmetryBreaking.kt
@@ -39,13 +39,13 @@ internal object SymmetryBreaking {
         objectiveIntVars: Set<Int> = emptySet(),
         objectiveBoolVars: Set<Int> = emptySet(),
         cancellation: Cancellation = Cancellation.Never,
-    ): Problem {
+    ): PassDelta {
         // Symmetry breaking is a one-shot transformation: once a [SymmetryHandling] factor is present
         // the generators have been found and posted. The presolve round engine re-enables this pass
         // whenever another pass changes the problem, but re-running would (a) re-search from scratch and
         // (b) have to remap (conjugate every generator) and re-key the heavy [SymmetryHandling] factor it
         // just added — an O(rounds) blow-up that dominated presolve on symmetric models. So detect once.
-        if (problem.factors.any { it is SymmetryHandling }) return problem
+        if (problem.factors.any { it is SymmetryHandling }) return PassDelta()
 
         // Generator-based detection: individualization–refinement over the unified variable+factor
         // colouring yields verified automorphism generators (catching composite and bool/int-mixed
@@ -60,13 +60,13 @@ internal object SymmetryBreaking {
         val scalarLex = scalarTotalOrders(problem, generators, objectiveIntVars, objectiveBoolVars)
         val valuePins = breakValueSymmetry(problem, objectiveIntVars, cancellation)
         if (generators.isEmpty() && scalarLex.isEmpty() && valuePins.isEmpty()) {
-            return problem
+            return PassDelta()
         }
         val extra = ArrayList<Factor>()
         if (generators.isNotEmpty()) extra.add(SymmetryHandling(generators))
         extra.addAll(scalarLex)
         extra.addAll(valuePins)
-        return PresolveShared.rebuildProblem(problem, problem.factors.toList() + extra)
+        return PassDelta(addedFactors = extra)
     }
 
     /**
@@ -205,12 +205,12 @@ internal object SymmetryBreaking {
      * Variables in [objectiveIntVars] are excluded (ordering them would change the optimum). Returns
      * the original problem unchanged when nothing is eligible.
      */
-    fun breakValuePrecedence(problem: Problem, objectiveIntVars: Set<Int> = emptySet()): Problem {
+    fun breakValuePrecedence(problem: Problem, objectiveIntVars: Set<Int> = emptySet()): PassDelta {
         val n = problem.numIntVars
         // A verified orbit is interchangeable; ordering its first occurrences is sound. A
         // fully-internal variable (domain ⊆ orbit) exists only when the orbit equals the whole
         // incidence group, so a split orbit simply posts nothing — never unsound.
-        val orbits = verifiedValueOrbits(problem) ?: return problem
+        val orbits = verifiedValueOrbits(problem) ?: return PassDelta()
         val extra = ArrayList<Factor>()
         for (orbit in orbits) {
             val orbitSet = orbit.toHashSet()
@@ -225,8 +225,8 @@ internal object SymmetryBreaking {
                 extra.add(ValuePrecede(sortedValues[i], sortedValues[i + 1], seqArray))
             }
         }
-        if (extra.isEmpty()) return problem
-        return PresolveShared.rebuildProblem(problem, problem.factors.toList() + extra)
+        if (extra.isEmpty()) return PassDelta()
+        return PassDelta(addedFactors = extra)
     }
 
     /** Refine a domain-incidence candidate [values] into verified-interchangeable value orbits: union
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/XorUnits.kt b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/XorUnits.kt
index ae7b154f9..89f0f3d43 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/presolve/XorUnits.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/presolve/XorUnits.kt
@@ -24,13 +24,13 @@ internal object XorUnits {
      * This is idempotent: units already present are not re-added, so the presolve round engine reaches
      * a fixpoint instead of appending duplicates on each round.
      */
-    fun deriveXorUnits(problem: Problem): Problem {
+    fun deriveXorUnits(problem: Problem): PassDelta {
         val xors = problem.factors.filterIsInstance<Xor>()
-        if (xors.isEmpty()) return problem
+        if (xors.isEmpty()) return PassDelta()
 
         val varOrder = LinkedHashSet<Int>()
         for (x in xors) for (lit in x.literals) varOrder.add(Lit.variable(lit))
-        if (varOrder.isEmpty()) return problem
+        if (varOrder.isEmpty()) return PassDelta()
         val vars = varOrder.toIntArray()
         val colOfVar = MutableIntIntMap(vars.size * 2)
         for (i in vars.indices) colOfVar.put(vars[i], i)
@@ -40,7 +40,7 @@ internal object XorUnits {
         // only their globally-implied root units go underived), mirroring the size guards on the other
         // presolve searches (clique merge, SAC probing). The reduction matters on small parity systems,
         // which stay far under the cap.
-        if (xors.size.toLong() * minOf(xors.size, vars.size) * words > XOR_ELIMINATION_WORK_CAP) return problem
+        if (xors.size.toLong() * minOf(xors.size, vars.size) * words > XOR_ELIMINATION_WORK_CAP) return PassDelta()
         val rows = Array(xors.size) { LongArray(words) }
         val rhs = IntArray(xors.size)
 
@@ -130,7 +130,7 @@ internal object XorUnits {
             }
         }
 
-        if (extra.isEmpty()) return problem
-        return PresolveShared.rebuildProblem(problem, problem.factors.toList() + extra)
+        if (extra.isEmpty()) return PassDelta()
+        return PassDelta(addedFactors = extra)
     }
 }
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/ClauseDb.kt b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/ClauseDb.kt
index 22dea90ae..284d4037d 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/ClauseDb.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/ClauseDb.kt
@@ -30,12 +30,14 @@ internal fun PropagationState.forEachBinaryPartner(lit: Int, action: (other: Int
     }
 }
 
-/** Unified factor accessor; routes static factor ids to [Problem.factors] and learned
- *  factor ids (≥ `problem.numFactors`) to [PropagationState.learnedClauses]. */
-internal fun PropagationState.factorAt(fid: Int): Propagator = if (fid < baseFactorCount) {
-    baseFactors[fid]
-} else {
-    learnedClauseStore[fid - baseFactorCount]
+/** Unified factor accessor; routes static factor ids to [Problem.factors], and tail ids
+ *  (≥ `baseFactorCount`) to the mid-life presolve store in [PropagationState.incremental] mode
+ *  (a tombstoned factor reads [NoPropagator]) or to [PropagationState.learnedClauses] otherwise. */
+internal fun PropagationState.factorAt(fid: Int): Propagator = when {
+    incremental && !factorAliveAt(fid) -> NoPropagator
+    fid < baseFactorCount -> baseFactors[fid]
+    incremental -> midlifeFactorStore[fid - baseFactorCount]
+    else -> learnedClauseStore[fid - baseFactorCount]
 }
 
 /**
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/Conflict.kt b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/Conflict.kt
index 33ce02db0..9d30967a2 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/Conflict.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/Conflict.kt
@@ -5,19 +5,20 @@ import com.eignex.klause.solver.Lit
 import com.eignex.klause.util.IntArrayList
 import com.eignex.klause.util.IntHashSet
 
-/** Boolean vars for factor [fid]: regular factors read from `problem.factors`; learned clauses
- *  (fid ≥ baseFactorCount) read from the ClausePropagator in `learnedClauseStore`. */
-private fun PropagationState.factorBoolVars(fid: Int): IntArray = if (fid < baseFactorCount) {
-    problem.factors[fid].boolVars
-} else {
-    learnedClauseStore[fid - baseFactorCount].boolVars
+/** Boolean vars for factor [fid]: base factors read from `problem.factors`; tail factors
+ *  (fid ≥ baseFactorCount) from `midlifeFactorList` in incremental mode, else from the
+ *  ClausePropagator in `learnedClauseStore`. */
+private fun PropagationState.factorBoolVars(fid: Int): IntArray = when {
+    fid < baseFactorCount -> problem.factors[fid].boolVars
+    incremental -> midlifeFactorList[fid - baseFactorCount].boolVars
+    else -> learnedClauseStore[fid - baseFactorCount].boolVars
 }
 
 /** Integer vars for factor [fid]: same routing as [factorBoolVars]. */
-private fun PropagationState.factorIntVars(fid: Int): IntArray = if (fid < baseFactorCount) {
-    problem.factors[fid].intVars
-} else {
-    learnedClauseStore[fid - baseFactorCount].intVars
+private fun PropagationState.factorIntVars(fid: Int): IntArray = when {
+    fid < baseFactorCount -> problem.factors[fid].intVars
+    incremental -> midlifeFactorList[fid - baseFactorCount].intVars
+    else -> learnedClauseStore[fid - baseFactorCount].intVars
 }
 
 /** Fallback conflict-levels collection for a failing propagator, routed through [factorBoolVars]/[factorIntVars]. */
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationResult.kt b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationResult.kt
index 396682155..cf138e50e 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationResult.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationResult.kt
@@ -176,10 +176,102 @@ sealed interface PropagationResult {
             append("})")
         }
 
+        /** Union this implied set with [other] by replaying everything from [other] over this base.
+         *  Bound tightenings take the tighter value; holes union; a variable pinned in the union is
+         *  dropped from the bound and hole sets. Used by root-bake probing to accumulate deductions. */
+        fun merge(other: Implied): Implied {
+            val bools = HashMap(bools)
+            other.forEachBool { k, v -> bools[k] = v }
+            val ints = HashMap(ints)
+            other.forEachInt { k, v -> ints[k] = v }
+            val mins = HashMap<Int, Int>()
+            forEachIntMin { k, v -> mins[k] = v }
+            other.forEachIntMin { k, v -> mins[k] = maxOf(mins[k] ?: Int.MIN_VALUE, v) }
+            val maxes = HashMap<Int, Int>()
+            forEachIntMax { k, v -> maxes[k] = v }
+            other.forEachIntMax { k, v -> maxes[k] = minOf(maxes[k] ?: Int.MAX_VALUE, v) }
+            val holes = HashSet<Long>()
+            forEachIntHole { id, v -> holes.add(packHole(id, v)) }
+            other.forEachIntHole { id, v -> holes.add(packHole(id, v)) }
+            for (k in ints.keys) {
+                mins.remove(k)
+                maxes.remove(k)
+                holes.removeAll { (it ushr HOLE_ID_SHIFT).toInt() == k }
+            }
+            return build(bools, ints, mins, maxes, holes)
+        }
+
+        /** This implied set with int [v]'s lower bound raised to at least [newMin]. */
+        fun withMin(v: Int, newMin: Int): Implied {
+            val mins = HashMap<Int, Int>()
+            forEachIntMin { k, vv -> mins[k] = vv }
+            mins[v] = maxOf(mins[v] ?: Int.MIN_VALUE, newMin)
+            val maxes = HashMap<Int, Int>()
+            forEachIntMax { k, vv -> maxes[k] = vv }
+            return build(bools, ints, mins, maxes, holeSet())
+        }
+
+        /** This implied set with int [v]'s upper bound lowered to at most [newMax]. */
+        fun withMax(v: Int, newMax: Int): Implied {
+            val mins = HashMap<Int, Int>()
+            forEachIntMin { k, vv -> mins[k] = vv }
+            val maxes = HashMap<Int, Int>()
+            forEachIntMax { k, vv -> maxes[k] = vv }
+            maxes[v] = minOf(maxes[v] ?: Int.MAX_VALUE, newMax)
+            return build(bools, ints, mins, maxes, holeSet())
+        }
+
+        /** This implied set with interior [value] excluded from int [v]'s domain (`v ≠ value`). */
+        fun withHole(v: Int, value: Int): Implied {
+            val mins = HashMap<Int, Int>()
+            forEachIntMin { k, vv -> mins[k] = vv }
+            val maxes = HashMap<Int, Int>()
+            forEachIntMax { k, vv -> maxes[k] = vv }
+            val holes = holeSet()
+            holes.add(packHole(v, value))
+            return build(bools, ints, mins, maxes, holes)
+        }
+
+        private fun holeSet(): HashSet<Long> {
+            val holes = HashSet<Long>()
+            forEachIntHole { id, v -> holes.add(packHole(id, v)) }
+            return holes
+        }
+
         /** Shared [PropagationResult] instances. */
         companion object {
+            private const val HOLE_ID_SHIFT = 32
+            private const val HOLE_VALUE_MASK = 0xFFFFFFFFL
+
+            private fun packHole(id: Int, value: Int): Long =
+                (id.toLong() shl HOLE_ID_SHIFT) or (value.toLong() and HOLE_VALUE_MASK)
+
+            /** Materialise an [Implied] from the accumulation maps used by [merge] / [withMin] / [withMax] /
+             *  [withHole], emitting the key-sorted parallel arrays the constructor expects. */
+            private fun build(
+                bools: Map<Int, Boolean>,
+                ints: Map<Int, Int>,
+                mins: Map<Int, Int>,
+                maxes: Map<Int, Int>,
+                holes: Set<Long>,
+            ): Implied {
+                val minK = mins.keys.toIntArray().also { it.sort() }
+                val maxK = maxes.keys.toIntArray().also { it.sort() }
+                val holesSorted = holes.toLongArray().also { it.sort() }
+                return Implied(
+                    bools = bools,
+                    ints = ints,
+                    intMinKeys = minK,
+                    intMinValues = IntArray(minK.size) { mins.getValue(minK[it]) },
+                    intMaxKeys = maxK,
+                    intMaxValues = IntArray(maxK.size) { maxes.getValue(maxK[it]) },
+                    intHoleVarIds = IntArray(holesSorted.size) { (holesSorted[it] ushr HOLE_ID_SHIFT).toInt() },
+                    intHoleValues = IntArray(holesSorted.size) { holesSorted[it].toInt() },
+                )
+            }
+
             /** The empty implied set (nothing forced). */
-            val Empty: Implied = Implied(IntArray(0), BooleanArray(0), IntArray(0), IntArray(0))
+            val EMPTY: Implied = Implied(IntArray(0), BooleanArray(0), IntArray(0), IntArray(0))
 
             /** Map-based factory. Call sites use `Implied(bools, ints)`; the constructor
              *  normalises to the primitive sorted-array form. Optional bound-tightening
@@ -197,7 +289,7 @@ sealed interface PropagationResult {
                 if (bools.isEmpty() && ints.isEmpty() &&
                     intMinKeys.isEmpty() && intMaxKeys.isEmpty() && intHoleVarIds.isEmpty()
                 ) {
-                    return Empty
+                    return EMPTY
                 }
                 val bKeys = bools.keys.toIntArray().also { it.sort() }
                 val bVals = BooleanArray(bKeys.size) { bools.getValue(bKeys[it]) }
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationSession.kt b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationSession.kt
index 70cacd17a..33bdebc4f 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationSession.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationSession.kt
@@ -430,7 +430,7 @@ class PropagationSession(
 
     private fun pushBool(v: Int, value: Boolean): PropagationResult {
         val want = if (value) 1 else 0
-        if (boolPinned[v] == want) return PropagationResult.Implied.Empty
+        if (boolPinned[v] == want) return PropagationResult.Implied.EMPTY
         val base = state.undoTop
         if (!state.pinBoolAsDecision(v, value)) return revertAndUnsat(state.conflictLevels ?: EmptyIntArray)
         val conflict = state.runToFixpoint(allFactors = false)
@@ -442,7 +442,7 @@ class PropagationSession(
     }
 
     private fun pushInt(v: Int, value: Int): PropagationResult {
-        if (intPinnedSet[v] && intPinnedVal[v] == value) return PropagationResult.Implied.Empty
+        if (intPinnedSet[v] && intPinnedVal[v] == value) return PropagationResult.Implied.EMPTY
         val base = state.undoTop
         if (!state.setIntAsDecision(v, value)) return revertAndUnsat(state.conflictLevels ?: EmptyIntArray)
         val conflict = state.runToFixpoint(allFactors = false)
@@ -600,7 +600,7 @@ class PropagationSession(
      */
     private fun impliedSince(base: Int): PropagationResult.Implied {
         val top = state.undoTop
-        if (top <= base) return PropagationResult.Implied.Empty
+        if (top <= base) return PropagationResult.Implied.EMPTY
         val bRaw = IntArrayList()
         val iRaw = IntArrayList()
         for (i in base until top) {
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationState.kt b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationState.kt
index 7dec9c06f..faf887ec2 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationState.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/propagation/PropagationState.kt
@@ -47,6 +47,15 @@ class PropagationState(
     /** The problem being propagated. */
     val problem: Problem,
     assumptions: Assumptions,
+    /**
+     * Incremental-presolve mode. When `true` the state supports mid-life factors — the
+     * presolve session appends factors and tombstones others between rounds via [addMidlifeFactor] /
+     * [tombstoneFactor] instead of rebuilding a fresh [Problem] each pass. The int-event
+     * machinery is forced on so a mid-life factor that subscribes to typed events wakes correctly even
+     * when the initial problem had no such factor. Defaults to `false`: a search state never adds
+     * presolve factors, so every allocation and branch below reduces to the exact prior behaviour.
+     */
+    internal val incremental: Boolean = false,
 ) {
     /** Two-bit-per-var three-valued pin store. [boolAssigned] says whether the variable has
      *  a definite value; [boolValueBits] holds the value when assigned (ignored otherwise).
@@ -92,6 +101,16 @@ class PropagationState(
     internal val dirtyInts: IntArrayDeque =
         IntArrayDeque(initialCapacity = problem.numIntVars.coerceAtLeast(8))
 
+    /** Whether the typed int-event machinery ([dirtyIntKinds] / [intEventWatchersBySlot]) is live.
+     *  On for any problem whose factors opt into it, and forced on in [incremental] mode so a
+     *  mid-life factor subscribing to typed events wakes even when the initial problem had none. */
+    private val eventMachineryOn: Boolean = problem.usesIntEventWatchers || incremental
+
+    /** Whether the per-factor dirty-variable delta accumulators are live. On for any problem with a
+     *  delta consumer, and forced on in [incremental] mode so a mid-life factor that consumes the delta
+     *  (a symmetry/structural pass can add e.g. a LexLess) gets its accumulator grown on the fly. */
+    private val deltaMachineryOn: Boolean = problem.usesIntEventDeltaConsumers || incremental
+
     /**
      * Per-int-var bitmask of the [IntEvent] kinds that occurred since the variable was last
      * drained — recorded by `markIntDirty` alongside [dirtyInts] and consumed (then cleared) by
@@ -105,7 +124,7 @@ class PropagationState(
      * mask already cleared — no stale bits survive a backtrack.
      */
     internal val dirtyIntKinds: IntArray =
-        if (problem.usesIntEventWatchers) IntArray(problem.numIntVars) else EmptyIntArray
+        if (eventMachineryOn) IntArray(problem.numIntVars) else EmptyIntArray
 
     // -------- Reusable propagation worklist (was allocated fresh per runToFixpoint) --------
     //
@@ -339,6 +358,13 @@ class PropagationState(
     internal val baseFactors: Array<out Propagator> = problem.propagators
     internal val baseFactorCount: Int = problem.factors.size
 
+    // Occurrence-list wakeup arrays cached off [problem] once at construction: they are now lazily
+    // built on [Problem] (deferred entirely for a presolve pass-view), so read them here — where a
+    // state is always over a fully-baked problem — to force them once instead of paying a delegated
+    // lazy access on every wakeup in the BCP hot loop.
+    private val nonBoolWatcherOcc: Array<IntArray> = problem.nonBoolWatcherBoolOccurrences
+    private val nonIntEventWatcherOcc: Array<IntArray> = problem.nonIntEventWatcherIntOccurrences
+
     /** Clauses learned during conflict analysis. */
     internal val learnedClauses: List<ClausePropagator> get() = learnedClauseStore
 
@@ -376,9 +402,41 @@ class PropagationState(
      *  to promote reused clauses and demote idle ones, then clears it for survivors. */
     internal val learnedUsedFlags: IntArrayList = IntArrayList()
 
+    // ---- Mid-life presolve factors ----
+    // A dedicated append-only store for factors added during an incremental presolve bake. Distinct
+    // from [learnedClauseStore]: a presolve state ([incremental]) never learns clauses and a search
+    // state never adds presolve factors, so at most one of the two tail stores is non-empty and both
+    // occupy the id range `[baseFactorCount, totalFactorCount)`. Ids are stable and never renumbered;
+    // dropping a factor (base or mid-life) tombstones its id ([tombstonedFactors]) and clears its
+    // [refPayload] slot. A tombstoned slot is NEVER reused by a later add — reuse would resurrect a
+    // stale propagator payload under a new factor id and silently corrupt a deduction (the
+    // wrong-optimum guard).
+    internal val midlifeFactorStore: ArrayList<Propagator> = ArrayList()
+
+    /** The [Factor] behind each mid-life propagator, parallel to [midlifeFactorStore]. Carried because
+     *  [Propagator] exposes no `boolVars` / `intVars`; the conflict and level machinery reads them here
+     *  for a mid-life factor the way it reads [Problem.factors] for a base one. */
+    internal val midlifeFactorList: ArrayList<Factor> = ArrayList()
+
+    /** Tombstoned factor ids (base or mid-life). [factorAt] returns [NoPropagator] for a member, so a
+     *  dropped factor is inert without removing it from the watcher indices — its id stays stable and
+     *  is never reused. Empty until the first drop, so a state that only appends allocates nothing. */
+    private val tombstonedFactors: IntHashSet = IntHashSet()
+
+    /** Delta overlay for occurrence-list bool wakeup of mid-life factors: `[v]` lists mid-life factor
+     *  ids that wake on any change to bool var `v` (those NOT using per-literal watchers). `null` until
+     *  the first such factor is added — a search state and a watcher-only presolve never allocate it,
+     *  so [enqueueForBoolChange] pays a single null-check. Complements [Problem.nonBoolWatcherBoolOccurrences]. */
+    private var midlifeBoolOccurrences: Array<IntArrayList>? = null
+
+    /** Int-side analog of [midlifeBoolOccurrences]: `[v]` lists mid-life factor ids that wake on any
+     *  change to int var `v` and do not subscribe to a typed int-event on `v`. Complements
+     *  [Problem.nonIntEventWatcherIntOccurrences]. */
+    private var midlifeIntOccurrences: Array<IntArrayList>? = null
+
     /** `problem.numFactors + learnedClauses.size`. Use this instead of `problem.numFactors`
      *  when iterating or sizing per-factor scratch in the engine. */
-    val totalFactorCount: Int get() = problem.numFactors + learnedClauseStore.size
+    val totalFactorCount: Int get() = problem.numFactors + learnedClauseStore.size + midlifeFactorStore.size
 
     /**
      * Per-literal wakeup index for factors opting into [Propagator.initialBoolWatchers].
@@ -441,7 +499,7 @@ class PropagationState(
      * the wake, which is sound).
      */
     internal val intEventWatchersBySlot: Array<IntArrayList> =
-        if (problem.usesIntEventWatchers) {
+        if (eventMachineryOn) {
             Array(problem.numIntVars * IntEvent.COUNT) { IntArrayList(initialCapacity = 1) }
         } else {
             emptyArray()
@@ -461,10 +519,24 @@ class PropagationState(
      * subscribed variable wakes the consumer and appends), which is the soundness-critical direction.
      * `null` per non-consuming factor; both arrays are empty when the problem has no consumer.
      */
-    private val eventDirtyVars: Array<IntArrayList?> =
-        if (problem.usesIntEventDeltaConsumers) arrayOfNulls(problem.numFactors) else emptyArray()
-    private val eventDirtyMark: Array<IntHashSet?> =
-        if (problem.usesIntEventDeltaConsumers) arrayOfNulls(problem.numFactors) else emptyArray()
+    // Grow-only (parallel to the factor store): [addMidlifeFactor] appends a slot per new factor so a
+    // mid-life delta consumer's accumulator stays in bounds. Empty when no consumer machinery is live.
+    private val eventDirtyVars: ArrayList<IntArrayList?> =
+        if (deltaMachineryOn) {
+            ArrayList<IntArrayList?>(
+                problem.numFactors,
+            ).apply { repeat(problem.numFactors) { add(null) } }
+        } else {
+            ArrayList()
+        }
+    private val eventDirtyMark: ArrayList<IntHashSet?> =
+        if (deltaMachineryOn) {
+            ArrayList<IntHashSet?>(
+                problem.numFactors,
+            ).apply { repeat(problem.numFactors) { add(null) } }
+        } else {
+            ArrayList()
+        }
 
     /**
      * Per-bool-var antecedent literals — the literal-form reason why this variable's
@@ -760,33 +832,99 @@ class PropagationState(
     val undoTop: Int get() = undoTag.size
 
     init {
-        for (fid in 0 until problem.numFactors) {
-            val propagator = problem.propagators[fid]
-            val watchers = propagator.initialBoolWatchers ?: continue
+        for (fid in 0 until problem.numFactors) registerFactor(fid, problem.propagators[fid])
+    }
+
+    /** Install factor [fid]'s static wakeup subscriptions into the per-literal / per-int-event advisor
+     *  indices and its delta-consumer accumulators. Factored out of the constructor loops so an
+     *  incremental presolve session can register a factor added mid-run without rebuilding the whole
+     *  state; the constructor just calls it once per initial factor. Order-preserving: appending in
+     *  factor-id order reproduces the original three-pass construction exactly. */
+    private fun registerFactor(fid: Int, propagator: Propagator) {
+        val watchers = propagator.initialBoolWatchers
+        if (watchers != null) {
             val blockers = propagator.initialBoolWatcherBlockers
-            for (i in watchers.indices) {
-                installLitWatch(watchers[i], fid, blockers?.getOrNull(i) ?: NO_BLOCKER)
-            }
+            for (i in watchers.indices) installLitWatch(watchers[i], fid, blockers?.getOrNull(i) ?: NO_BLOCKER)
+        }
+        if (eventMachineryOn) {
+            propagator.initialIntEventWatches?.let { for (packed in it) intEventWatchersBySlot[packed].add(fid) }
+        }
+        if (deltaMachineryOn && propagator.consumesIntEventDelta) {
+            eventDirtyVars[fid] = IntArrayList()
+            eventDirtyMark[fid] = IntHashSet()
         }
     }
 
-    init {
-        if (problem.usesIntEventWatchers) {
-            for (fid in 0 until problem.numFactors) {
-                val watches = problem.propagators[fid].initialIntEventWatches ?: continue
-                for (packed in watches) intEventWatchersBySlot[packed].add(fid)
-            }
+    /** True iff factor id [fid] has not been tombstoned. */
+    internal fun factorAliveAt(fid: Int): Boolean = fid !in tombstonedFactors
+
+    /**
+     * Append presolve [factor] to the live state as a mid-life factor and return its stable id.
+     * Installs its watcher subscriptions ([registerFactor]) and its occurrence-list wakeup overlay
+     * ([registerMidlifeOccurrences]), and grows [refPayload] by one slot so the factor's
+     * `state.refPayload[fid]` access stays in bounds. The factor does NOT fire here; the session drives
+     * a [runToFixpoint] afterwards (seeding it via `initialFactor` or `allFactors`).
+     *
+     * Only valid in [incremental] mode. A factor that consumes the int-event delta (a symmetry or
+     * structural pass can add one) is supported: the per-factor accumulators grow by one slot here so
+     * [registerFactor] can install it, and the delta machinery is always live in incremental mode.
+     */
+    internal fun addMidlifeFactor(factor: Factor): Int {
+        require(incremental) { "mid-life factors require an incremental PropagationState" }
+        val prop = factor.asPropagator()
+        val fid = totalFactorCount
+        midlifeFactorStore.add(prop)
+        midlifeFactorList.add(factor)
+        refPayloadStore.add(null)
+        // Grow the delta accumulators in lockstep so a mid-life consumer's `eventDirtyVars[fid]` slot
+        // exists before [registerFactor] populates it (delta machinery is always live in incremental mode).
+        if (deltaMachineryOn) {
+            eventDirtyVars.add(null)
+            eventDirtyMark.add(null)
         }
+        if (prop is ClausePropagator && prop.literals.size == 2) binaryClauseCount++
+        registerFactor(fid, prop)
+        registerMidlifeOccurrences(fid, factor, prop)
+        return fid
     }
 
-    init {
-        if (problem.usesIntEventDeltaConsumers) {
-            for (fid in 0 until problem.numFactors) {
-                if (problem.propagators[fid].consumesIntEventDelta) {
-                    eventDirtyVars[fid] = IntArrayList()
-                    eventDirtyMark[fid] = IntHashSet()
-                }
+    /**
+     * Tombstone factor [fid] (base or mid-life): mark it dropped ([factorAt] then returns [NoPropagator],
+     * so it never fires again) and clear its [refPayload] slot. The id is retired, never reused — the
+     * slot must stay cleared so a later add can't inherit a stale payload (the wrong-optimum guard). The
+     * factor's entries linger in the watcher indices and occurrence lists; they wake a [NoPropagator],
+     * a no-op.
+     */
+    internal fun tombstoneFactor(fid: Int) {
+        require(incremental) { "tombstoning requires an incremental PropagationState" }
+        if (!tombstonedFactors.add(fid)) return
+        refPayloadStore[fid] = null
+    }
+
+    /**
+     * Register mid-life factor [fid]'s occurrence-list wakeup, mirroring [Problem.nonBoolWatcherBoolOccurrences]
+     * / [Problem.nonIntEventWatcherIntOccurrences]: a factor using per-literal bool watchers is excluded
+     * from every bool var's overlay (it wakes through [boolWatchersByLit]); on the int side a var is
+     * excluded only when the factor subscribes to a typed event on *that* var. The overlays are allocated
+     * lazily on first need.
+     */
+    private fun registerMidlifeOccurrences(fid: Int, factor: Factor, prop: Propagator) {
+        if (prop === NoPropagator) return
+        if (prop.initialBoolWatchers == null) {
+            val occ = midlifeBoolOccurrences ?: Array(
+                problem.numBoolVars,
+            ) { IntArrayList() }.also { midlifeBoolOccurrences = it }
+            for (v in factor.boolVars) occ[v].add(fid)
+        }
+        val intVars = factor.intVars
+        if (intVars.isNotEmpty()) {
+            val watched: IntHashSet? = prop.initialIntEventWatches?.let { ws ->
+                IntHashSet(ws.size).apply { for (w in ws) add(IntEvent.intVarOf(w)) }
             }
+            val occ = midlifeIntOccurrences ?: Array(
+                problem.numIntVars,
+            ) { IntArrayList() }.also { midlifeIntOccurrences = it }
+            for (v in intVars) if (watched?.contains(v) != true) occ[v].add(fid)
         }
     }
 
@@ -894,6 +1032,7 @@ class PropagationState(
     internal fun runToFixpoint(
         allFactors: Boolean,
         initialFactor: Int = -1,
+        initialFactors: IntArray = EmptyIntArray,
         cancellation: Cancellation = Cancellation.Never,
     ): IntArray? {
         // Clear conflict bookkeeping from any prior run — reusing the state across pushes
@@ -925,6 +1064,9 @@ class PropagationState(
             // otherwise sit dormant since the watcher index only wakes on false-going
             // literals, and a freshly-added clause's watches haven't been triggered yet).
             if (initialFactor in 0 until factorCount) propEnq(initialFactor)
+            // Seed a batch of freshly-added mid-life factors so each fires once on the next cycle;
+            // like [initialFactor], their watches haven't been triggered yet so they'd sit dormant.
+            for (fid in initialFactors) if (fid in 0 until factorCount) propEnq(fid)
         }
         while (propQueue.isNotEmpty()) {
             if (allFactors && (fireCount++ and CANCEL_POLL_MASK) == 0 && cancellation()) return null
@@ -948,7 +1090,15 @@ class PropagationState(
                     maxLevelForClause(f.literals)
                 }
             } else {
-                val factor = problem.factors[fid]
+                // A base factor reads its vars from the immutable problem; a mid-life presolve factor
+                // (fid >= baseFactorCount, only in [incremental] mode) from [midlifeFactorList].
+                val factor = if (fid <
+                    baseFactorCount
+                ) {
+                    problem.factors[fid]
+                } else {
+                    midlifeFactorList[fid - baseFactorCount]
+                }
                 maxLevelForVars(factor.boolVars, factor.intVars)
             }
             currentFactor = fid
@@ -987,7 +1137,12 @@ class PropagationState(
      * literals satisfy the clause, no propagation needed.
      */
     private fun enqueueForBoolChange(v: Int) {
-        for (fid in problem.nonBoolWatcherBoolOccurrences[v]) propEnq(fid)
+        for (fid in nonBoolWatcherOcc[v]) propEnq(fid)
+        // Mid-life presolve factors waking via occurrence lists; null (no overlay) otherwise.
+        midlifeBoolOccurrences?.let {
+            val list = it[v]
+            for (i in 0 until list.size) propEnq(list[i])
+        }
         // The literal that just became false is the one whose polarity opposes the pin.
         // The var is assigned here (added to dirtyBools only after a successful pin), so read
         // the packed value bit directly instead of the boxing `boolValues[v]` accessor.
@@ -1030,7 +1185,12 @@ class PropagationState(
      * occurrence-list walk over [com.eignex.klause.solver.Problem.intOccurrences].
      */
     private fun enqueueForIntChange(v: Int) {
-        for (fid in problem.nonIntEventWatcherIntOccurrences[v]) propEnq(fid)
+        for (fid in nonIntEventWatcherOcc[v]) propEnq(fid)
+        // Mid-life presolve factors waking via occurrence lists; null (no overlay) otherwise.
+        midlifeIntOccurrences?.let {
+            val list = it[v]
+            for (i in 0 until list.size) propEnq(list[i])
+        }
         if (dirtyIntKinds.isEmpty()) return
         val mask = dirtyIntKinds[v]
         if (mask == 0) return
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/solver/Problem.kt b/klause/src/commonMain/kotlin/com/eignex/klause/solver/Problem.kt
index f386f047e..9dd6fc60c 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/solver/Problem.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/solver/Problem.kt
@@ -8,7 +8,6 @@ import com.eignex.klause.propagation.extractConflictBools
 import com.eignex.klause.propagation.extractConflictFactors
 import com.eignex.klause.propagation.extractConflictInts
 import com.eignex.klause.util.IntArrayList
-import kotlin.random.Random
 
 /**
  * Immutable solver-side problem. Variables come in two id spaces:
@@ -32,54 +31,14 @@ class Problem(
     /** The constraints over the variables. */
     val factors: Array<Factor>,
     /**
-     * Opt-in failed-literal probing at bake time. When `true`, every free bool variable is
-     * tested with both polarities: if pinning one polarity propagates Unsat, the other
-     * polarity is permanently folded into [baked]. Iterated to a fixed point. Cost is
-     * `O(numFreeBools × propagate)` once at construction; the result is a tighter baseline
-     * for every subsequent session. Off by default — tests construct many small problems
-     * and don't want the construction overhead.
+     * Extra root deductions computed outside the kernel — the failed-literal / SAC probing tiers now
+     * live in [com.eignex.klause.presolve.RootBaker], which runs them against an already-base-baked
+     * [Problem] and feeds the result back here. Merged into the base `propagate(Assumptions.None)`
+     * bake before it folds into [intDomains], so the extra pins / bound tightenings / holes become
+     * part of [baked] and the problem's own domains. Defaults to empty = base bake only; the kernel
+     * never initiates probing itself (that would create a `solver → presolve → solver` cycle).
      */
-    val probeFailedLiterals: Boolean = false,
-    /**
-     * Opt-in bound-SAC (singleton arc consistency) probing at bake time. After
-     * [probeFailedLiterals] settles, every int var with a multi-value domain has its
-     * min and max probed: pin the bound, propagate, and if Unsat, tighten the bound by
-     * one and loop. Captures bound-level deductions the per-call propagator misses
-     * because they require hypothetical reasoning across factors. Cost is
-     * `O(Σ |dom(v)|_extreme × propagate)`; result rides in [baked] as bound
-     * tightenings (non-singleton) and pins (when SAC narrows a var to a single value).
-     * Interior-hole SAC (probing values strictly between min and max) is left for a
-     * follow-up — it needs Implied/Assumptions to carry hole sets too.
-     */
-    val probeIntBounds: Boolean = false,
-    /**
-     * Opt-in interior-hole SAC. Builds on [probeIntBounds]: after bound-SAC settles,
-     * each multi-value int var has its interior values (strictly between current min
-     * and max) probed; on Unsat the value is recorded as an interior hole in [baked].
-     * Cost is `O(Σ |dom(v)| × propagate)` per pass; use sparingly on large domains.
-     * Implies [probeIntBounds].
-     */
-    val probeIntHoles: Boolean = false,
-    /**
-     * Cap on per-var probe calls during bake-time SAC. After this many `propagate` calls
-     * targeting one var (across both bound and hole probing), the loop stops probing
-     * that var for the remainder of the bake. Defaults to unlimited; set to a small
-     * positive number for very wide domains to prevent pathological construction cost.
-     */
-    val probeBudgetPerVar: Int = Int.MAX_VALUE,
-    /**
-     * Cap on total probe calls across all vars and all SAC passes during bake. Once
-     * exceeded, the SAC loops exit gracefully with whatever tightenings they've
-     * accumulated so far. Unlimited by default.
-     */
-    val probeTotalBudget: Int = Int.MAX_VALUE,
-    /**
-     * Seed for the RNG that breaks ties in the wdeg-weighted SAC probe order. Equal-score
-     * vars get a random permutation each outer pass so a fixed-point loop on a flat
-     * weight landscape doesn't keep visiting the same first var. Deterministic for a
-     * given seed.
-     */
-    val probeSeed: Long = 0L,
+    seedDeductions: PropagationResult = PropagationResult.Implied.EMPTY,
     /**
      * Cooperative-cancellation token for the construction-time bake ([baked]). Polled on the
      * full-propagation fixpoint and between SAC passes so a `-t` deadline can abort an
@@ -105,6 +64,16 @@ class Problem(
      * is redundant and the two can interact.
      */
     val hasSymmetryBreaking: Boolean = false,
+    /**
+     * Presolve pass-view mode. When `true`, this [Problem] is a cheap carrier of `(factors, intDomains)`
+     * for a presolve pass that reads only those two: the eager derived structures — [propagators],
+     * the occurrence lists, and the root [baked] fold — are deferred to first access and NOT forced at
+     * construction, and [intDomains] are taken to be *already folded* (the incremental
+     * [com.eignex.klause.presolve.PresolveSession] supplies its re-propagated domains). Off by
+     * default: every solver/LS/LP consumer builds a normal [Problem] whose [baked] is forced eagerly at
+     * construction exactly as before, so nothing outside presolve sees a behavioural change.
+     */
+    val preFolded: Boolean = false,
 ) {
     /**
      * Domain (bounds) of each integer variable, indexed by int var id. A defensive copy of
@@ -121,7 +90,9 @@ class Problem(
     /** Propagator objects for the CP engine, one per factor. Factors that have been structurally
      *  split return a dedicated propagator instance from [Factor.asPropagator]; unsplit factors
      *  return themselves. Computed once at construction. */
-    val propagators: Array<out Propagator> = Array(factors.size) { factors[it].asPropagator() }
+    val propagators: Array<out Propagator> by lazy(LazyThreadSafetyMode.NONE) {
+        Array(factors.size) { factors[it].asPropagator() }
+    }
 
     /** Invariant objects for the LS engine, one per factor. Factors that have been structurally
      *  split return a dedicated invariant instance from [Factor.asInvariant]; unsplit factors
@@ -150,29 +121,21 @@ class Problem(
         numIntVars: Int,
         intDomains: Array<IntDomain>,
         factors: List<Factor>,
-        probeFailedLiterals: Boolean = false,
-        probeIntBounds: Boolean = false,
-        probeIntHoles: Boolean = false,
-        probeBudgetPerVar: Int = Int.MAX_VALUE,
-        probeTotalBudget: Int = Int.MAX_VALUE,
-        probeSeed: Long = 0L,
+        seedDeductions: PropagationResult = PropagationResult.Implied.EMPTY,
         cancellation: Cancellation = Cancellation.Never,
         impliedFactorMask: BooleanArray? = null,
         hasSymmetryBreaking: Boolean = false,
+        preFolded: Boolean = false,
     ) : this(
         numBoolVars = numBoolVars,
         numIntVars = numIntVars,
         intDomains = intDomains,
         factors = Array(factors.size) { factors[it] },
-        probeFailedLiterals = probeFailedLiterals,
-        probeIntBounds = probeIntBounds,
-        probeIntHoles = probeIntHoles,
-        probeBudgetPerVar = probeBudgetPerVar,
-        probeTotalBudget = probeTotalBudget,
-        probeSeed = probeSeed,
+        seedDeductions = seedDeductions,
         cancellation = cancellation,
         impliedFactorMask = impliedFactorMask,
         hasSymmetryBreaking = hasSymmetryBreaking,
+        preFolded = preFolded,
     )
 
     /**
@@ -180,7 +143,9 @@ class Problem(
      * LS-side lists force [invariants] lazily, so a presolve/CP-only problem never builds them. The
      * individual lists below delegate here; access them by name or through this index directly.
      */
-    val occurrences: OccurrenceIndex = OccurrenceIndex(numBoolVars, numIntVars, factors, propagators) { invariants }
+    val occurrences: OccurrenceIndex by lazy(LazyThreadSafetyMode.NONE) {
+        OccurrenceIndex(numBoolVars, numIntVars, factors, propagators) { invariants }
+    }
 
     /** Deductive occurrence lists over Boolean variables. See [OccurrenceIndex.boolOccurrences]. */
     val boolOccurrences: Array<IntArray> get() = occurrences.boolOccurrences
@@ -211,18 +176,29 @@ class Problem(
     val numFactors: Int get() = factors.size
 
     /**
-     * Result of running [propagate] once with empty assumptions at construction time. Caches
-     * literals/values forced by the constraints alone — every solver call gets a smaller
-     * residual problem with no per-call propagation cost, and trivially-Unsat problems surface
-     * here instead of after a full search budget. May be [PropagationResult.Unsat] for
-     * trivially-infeasible problems; callers that want fail-fast behavior can check this.
+     * Result of running [propagate] once with empty assumptions at construction time, merged with
+     * any [seedDeductions] the presolve-lane probing supplied. Caches literals/values forced by the
+     * constraints alone — every solver call gets a smaller residual problem with no per-call
+     * propagation cost, and trivially-Unsat problems surface here instead of after a full search
+     * budget. May be [PropagationResult.Unsat] for trivially-infeasible problems; callers that want
+     * fail-fast behavior can check this.
      *
      * The deductions recorded here are also folded back into [intDomains], so the diff is
      * expressed relative to the constructor-input domains rather than the tightened ones.
      * Re-seeding it on an already-tightened domain is a no-op, so existing consumers that
      * replay [baked] as assumptions are unaffected.
      */
-    val baked: PropagationResult = computeBaked().also(::foldIntoDomains)
+    val baked: PropagationResult by lazy(LazyThreadSafetyMode.NONE) {
+        mergeBase(propagate(Assumptions.None, cancellation), seedDeductions)
+    }
+
+    // Force the root bake and fold its deductions into [intDomains] eagerly — except in [preFolded]
+    // pass-view mode, where the domains are already folded and the deferred derived structures stay
+    // uncomputed. A non-preFolded [Problem] thus behaves exactly as before (baked + folded at
+    // construction); this init access is what forces the otherwise-lazy propagators/occurrences/baked.
+    init {
+        if (!preFolded) foldIntoDomains(baked)
+    }
 
     /** Folds the root-level int deductions of a successful bake into [intDomains] so the
      *  tightened bounds are part of the problem itself rather than transient solver state.
@@ -249,338 +225,21 @@ class Problem(
         }
     }
 
-    private fun computeBaked(): PropagationResult {
-        val initial = propagate(Assumptions.None, cancellation)
-        if (initial is PropagationResult.Unsat) return initial
-        var result: PropagationResult = initial
-        // SAC probing fires `propagate` repeatedly; stop entering new probe phases once the
-        // bake deadline has passed (each phase below also polls between its own probes).
-        if (cancellation()) return result
-        if (probeFailedLiterals) {
-            result = probeFreeBools(result as PropagationResult.Implied)
-            if (result is PropagationResult.Unsat) return result
-        }
-        if (probeIntBounds || probeIntHoles) {
-            // wdeg state shared across bound-SAC and hole-SAC: a probe failure under bound-SAC
-            // raises factor weights that then steer hole-SAC's first iteration, and vice versa.
-            val factorWeights = DoubleArray(factors.size) { 1.0 }
-            val rng = Random(probeSeed)
-            result = probeBoundSac(result as PropagationResult.Implied, factorWeights, rng)
-            if (result is PropagationResult.Unsat) return result
-            if (probeIntHoles) {
-                result = probeIntHoles(result as PropagationResult.Implied, factorWeights, rng)
-            }
-        }
-        return result
-    }
-
-    /** Interior-value SAC: probe every value strictly between each multi-value int var's
-     *  current min and max. Iterates with bound-SAC interleaved so that hole-discovered
-     *  tightenings can lift bounds and vice versa. */
-    private fun probeIntHoles(
-        base: PropagationResult.Implied,
-        factorWeights: DoubleArray,
-        rng: Random,
-    ): PropagationResult {
-        var acc: PropagationResult.Implied = base
-        val perVarCalls = IntArray(numIntVars)
-        var totalCalls = 0
-        var changed = true
-        while (changed) {
-            changed = false
-            for (v in sacProbeOrder(acc, factorWeights, rng)) {
-                if (cancellation()) return acc
-                if (acc.intValueOrNull(v) != null) continue
-                if (perVarCalls[v] >= probeBudgetPerVar) continue
-                if (totalCalls >= probeTotalBudget) return acc
-                val orig = intDomains[v]
-                val curMin = acc.intMinOrNullCompat(v) ?: orig.min
-                val curMax = acc.intMaxOrNullCompat(v) ?: orig.max
-                if (curMin >= curMax) continue
-                val accAsAssumptions = acc.toAssumptions()
-                // Build a per-var hole-set once so the `alreadyHole` lookup in the k-loop
-                // is O(1) instead of a linear scan of acc.intHoleVarIds for every probed k.
-                val existingHoles = HashSet<Int>()
-                for (i in 0 until acc.intHoleVarIds.size) {
-                    if (acc.intHoleVarIds[i] == v) existingHoles.add(acc.intHoleValues[i])
-                }
-                for (k in (curMin + 1) until curMax) {
-                    if (perVarCalls[v] >= probeBudgetPerVar) break
-                    if (totalCalls >= probeTotalBudget) return acc
-                    if (k !in orig) continue
-                    if (k in existingHoles) continue
-                    perVarCalls[v]++
-                    totalCalls++
-                    val pin = propagate(accAsAssumptions.withInt(v, k), cancellation)
-                    if (pin is PropagationResult.Unsat) {
-                        bumpFactorWeights(pin, factorWeights)
-                        perVarCalls[v]++
-                        totalCalls++
-                        val r = propagate(accAsAssumptions.withIntHole(v, k), cancellation)
-                        if (r is PropagationResult.Unsat) return r
-                        acc = addHoleToImplied(acc, v, k)
-                        acc = mergeImplied(acc, r as PropagationResult.Implied)
-                        changed = true
-                    }
-                }
-            }
-        }
-        return acc
-    }
+    /** Merge the presolve-lane [seed] deductions into the kernel's [base] `propagate` bake. An
+     *  `Unsat` on either side wins (an infeasible base or a probing-proven contradiction), otherwise
+     *  the two implied sets union via [PropagationResult.Implied.merge]. The common no-probe case
+     *  passes [PropagationResult.Implied.EMPTY] and returns [base] unchanged. */
+    private fun mergeBase(base: PropagationResult, seed: PropagationResult): PropagationResult = when {
+        base is PropagationResult.Unsat -> base
 
-    private fun addHoleToImplied(a: PropagationResult.Implied, v: Int, value: Int): PropagationResult.Implied {
-        val holeSet = HashSet<Long>()
-        a.forEachIntHole { id, vv ->
-            holeSet.add((id.toLong() shl 32) or (vv.toLong() and 0xFFFFFFFFL))
-        }
-        holeSet.add((v.toLong() shl 32) or (value.toLong() and 0xFFFFFFFFL))
-        val sorted = holeSet.toLongArray().also { it.sort() }
-        val ids = IntArray(sorted.size) { (sorted[it] ushr 32).toInt() }
-        val vals = IntArray(sorted.size) { sorted[it].toInt() }
-        val mins = HashMap<Int, Int>()
-        a.forEachIntMin { k, vv -> mins[k] = vv }
-        val maxes = HashMap<Int, Int>()
-        a.forEachIntMax { k, vv -> maxes[k] = vv }
-        val minK = mins.keys.toIntArray().also { it.sort() }
-        val maxK = maxes.keys.toIntArray().also { it.sort() }
-        return PropagationResult.Implied(
-            bools = a.bools,
-            ints = a.ints,
-            intMinKeys = minK,
-            intMinValues = IntArray(minK.size) { mins.getValue(minK[it]) },
-            intMaxKeys = maxK,
-            intMaxValues = IntArray(maxK.size) { maxes.getValue(maxK[it]) },
-            intHoleVarIds = ids,
-            intHoleValues = vals,
-        )
-    }
+        seed is PropagationResult.Unsat -> seed
 
-    /** Probe-order heuristic: wdeg / dom — sort descending by `Σ factorWeights[f] / dom(v)`
-     *  so the budget is spent first on vars that are heavily-constrained relative to their
-     *  remaining domain. Each Unsat probe bumps the weights of the factors in its conflict
-     *  via [bumpFactorWeights], so failing probes steer the next pass toward related vars
-     *  (the classic wdeg adaptation). Ties break by a per-pass random key (deterministic
-     *  for a given [probeSeed]) — this avoids the deterministic-id-order bias that the
-     *  prior dom-sized order would inherit when every var has the same dom and weight. */
-    private fun sacProbeOrder(acc: PropagationResult.Implied, factorWeights: DoubleArray, rng: Random): IntArray {
-        val scores = DoubleArray(numIntVars) { v ->
-            if (acc.intValueOrNull(v) != null) return@DoubleArray Double.NEGATIVE_INFINITY
-            val orig = intDomains[v]
-            val lo = acc.intMinOrNullCompat(v) ?: orig.min
-            val hi = acc.intMaxOrNullCompat(v) ?: orig.max
-            val dom = (hi - lo + 1).coerceAtLeast(1)
-            var wdeg = 0.0
-            val occ = intOccurrences[v]
-            for (i in occ.indices) wdeg += factorWeights[occ[i]]
-            wdeg / dom
-        }
-        val tie = IntArray(numIntVars) { rng.nextInt() }
-        val boxed = Array(numIntVars) { it }
-        boxed.sortWith(
-            Comparator { a, b ->
-                val sa = scores[a]
-                val sb = scores[b]
-                if (sa != sb) sb.compareTo(sa) else tie[a].compareTo(tie[b])
-            },
-        )
-        return IntArray(numIntVars) { boxed[it] }
-    }
-
-    /** Bump every factor implicated in an Unsat conflict by 1.0. This is the wdeg update
-     *  rule: factors that repeatedly fail under hypothetical pins gain weight and steer
-     *  the SAC probe order toward the vars they mention on subsequent passes. */
-    private fun bumpFactorWeights(unsat: PropagationResult.Unsat, factorWeights: DoubleArray) {
-        for (f in unsat.conflictFactors) {
-            if (f in factorWeights.indices) factorWeights[f] += 1.0
-        }
-    }
-
-    /**
-     * Bound-SAC fixed-point loop. Probes the min and max of each multi-value int var
-     * under the current [base]; an Unsat result lets us tighten that bound by one
-     * and re-probe. Returns the strengthened [PropagationResult.Implied], or `Unsat`
-     * if the problem turns out to be infeasible.
-     */
-    private fun probeBoundSac(
-        base: PropagationResult.Implied,
-        factorWeights: DoubleArray,
-        rng: Random,
-    ): PropagationResult {
-        var acc: PropagationResult.Implied = base
-        val perVarCalls = IntArray(numIntVars)
-        var totalCalls = 0
-        var changed = true
-        while (changed) {
-            changed = false
-            for (v in sacProbeOrder(acc, factorWeights, rng)) {
-                if (cancellation()) return acc
-                if (acc.intValueOrNull(v) != null) continue
-                if (perVarCalls[v] >= probeBudgetPerVar) continue
-                if (totalCalls >= probeTotalBudget) return acc
-                val orig = intDomains[v]
-                val curMin = acc.intMinOrNullCompat(v) ?: orig.min
-                val curMax = acc.intMaxOrNullCompat(v) ?: orig.max
-                if (curMin >= curMax) continue
-                val accAsAssumptions = acc.toAssumptions()
-                perVarCalls[v]++
-                totalCalls++
-                val pinMin = propagate(accAsAssumptions.withInt(v, curMin), cancellation)
-                if (pinMin is PropagationResult.Unsat) {
-                    bumpFactorWeights(pinMin, factorWeights)
-                    perVarCalls[v]++
-                    totalCalls++
-                    val tightened = accAsAssumptions.withTightenedMin(v, curMin + 1)
-                    val r = propagate(tightened, cancellation)
-                    if (r is PropagationResult.Unsat) return r
-                    acc = addMinToImplied(acc, v, curMin + 1)
-                    acc = mergeImplied(acc, r as PropagationResult.Implied)
-                    changed = true
-                    continue
-                }
-                if (perVarCalls[v] >= probeBudgetPerVar) continue
-                if (totalCalls >= probeTotalBudget) return acc
-                perVarCalls[v]++
-                totalCalls++
-                val pinMax = propagate(accAsAssumptions.withInt(v, curMax), cancellation)
-                if (pinMax is PropagationResult.Unsat) {
-                    bumpFactorWeights(pinMax, factorWeights)
-                    perVarCalls[v]++
-                    totalCalls++
-                    val tightened = accAsAssumptions.withTightenedMax(v, curMax - 1)
-                    val r = propagate(tightened, cancellation)
-                    if (r is PropagationResult.Unsat) return r
-                    acc = addMaxToImplied(acc, v, curMax - 1)
-                    acc = mergeImplied(acc, r as PropagationResult.Implied)
-                    changed = true
-                }
-            }
-        }
-        return acc
-    }
-
-    private fun addMinToImplied(a: PropagationResult.Implied, v: Int, newMin: Int): PropagationResult.Implied {
-        val mins = HashMap<Int, Int>()
-        a.forEachIntMin { k, vv -> mins[k] = vv }
-        mins[v] = maxOf(mins[v] ?: Int.MIN_VALUE, newMin)
-        val maxes = HashMap<Int, Int>()
-        a.forEachIntMax { k, vv -> maxes[k] = vv }
-        val minK = mins.keys.toIntArray().also { it.sort() }
-        val maxK = maxes.keys.toIntArray().also { it.sort() }
-        return PropagationResult.Implied(
-            bools = a.bools,
-            ints = a.ints,
-            intMinKeys = minK,
-            intMinValues = IntArray(minK.size) { mins.getValue(minK[it]) },
-            intMaxKeys = maxK,
-            intMaxValues = IntArray(maxK.size) { maxes.getValue(maxK[it]) },
-            intHoleVarIds = a.intHoleVarIds.copyOf(),
-            intHoleValues = a.intHoleValues.copyOf(),
-        )
-    }
-
-    private fun addMaxToImplied(a: PropagationResult.Implied, v: Int, newMax: Int): PropagationResult.Implied {
-        val mins = HashMap<Int, Int>()
-        a.forEachIntMin { k, vv -> mins[k] = vv }
-        val maxes = HashMap<Int, Int>()
-        a.forEachIntMax { k, vv -> maxes[k] = vv }
-        maxes[v] = minOf(maxes[v] ?: Int.MAX_VALUE, newMax)
-        val minK = mins.keys.toIntArray().also { it.sort() }
-        val maxK = maxes.keys.toIntArray().also { it.sort() }
-        return PropagationResult.Implied(
-            bools = a.bools,
-            ints = a.ints,
-            intMinKeys = minK,
-            intMinValues = IntArray(minK.size) { mins.getValue(minK[it]) },
-            intMaxKeys = maxK,
-            intMaxValues = IntArray(maxK.size) { maxes.getValue(maxK[it]) },
-            intHoleVarIds = a.intHoleVarIds.copyOf(),
-            intHoleValues = a.intHoleValues.copyOf(),
-        )
-    }
-
-    /** Union two `Implied`s by replaying everything from `b` into the `a` base. */
-    private fun mergeImplied(a: PropagationResult.Implied, b: PropagationResult.Implied): PropagationResult.Implied {
-        val bools = HashMap(a.bools)
-        b.forEachBool { k, v -> bools[k] = v }
-        val ints = HashMap(a.ints)
-        b.forEachInt { k, v -> ints[k] = v }
-        val mins = HashMap<Int, Int>()
-        a.forEachIntMin { k, v -> mins[k] = v }
-        b.forEachIntMin { k, v -> mins[k] = maxOf(mins[k] ?: Int.MIN_VALUE, v) }
-        val maxes = HashMap<Int, Int>()
-        a.forEachIntMax { k, v -> maxes[k] = v }
-        b.forEachIntMax { k, v -> maxes[k] = minOf(maxes[k] ?: Int.MAX_VALUE, v) }
-        // Holes — union.
-        val holes = HashSet<Long>()
-        a.forEachIntHole { id, v -> holes.add((id.toLong() shl 32) or (v.toLong() and 0xFFFFFFFFL)) }
-        b.forEachIntHole { id, v -> holes.add((id.toLong() shl 32) or (v.toLong() and 0xFFFFFFFFL)) }
-        // Drop now-pinned vars from the bound and hole sets.
-        for (k in ints.keys) {
-            mins.remove(k)
-            maxes.remove(k)
-            holes.removeAll { (it ushr 32).toInt() == k }
-        }
-        val minK = mins.keys.toIntArray().also { it.sort() }
-        val maxK = maxes.keys.toIntArray().also { it.sort() }
-        val holesSorted = holes.toLongArray().also { it.sort() }
-        val holeIds = IntArray(holesSorted.size) { (holesSorted[it] ushr 32).toInt() }
-        val holeVals = IntArray(holesSorted.size) { holesSorted[it].toInt() }
-        return PropagationResult.Implied(
-            bools = bools,
-            ints = ints,
-            intMinKeys = minK,
-            intMinValues = IntArray(minK.size) { mins.getValue(minK[it]) },
-            intMaxKeys = maxK,
-            intMaxValues = IntArray(maxK.size) { maxes.getValue(maxK[it]) },
-            intHoleVarIds = holeIds,
-            intHoleValues = holeVals,
-        )
-    }
-
-    /**
-     * Iteratively strengthens [initial] by probing each free bool with both polarities. If
-     * one polarity is Unsat under the current accumulated base, the opposite polarity is
-     * forced. Repeats until a full pass finds no new forcings.
-     */
-    private fun probeFreeBools(initial: PropagationResult.Implied): PropagationResult {
-        val bools = HashMap(initial.bools)
-        val ints = HashMap(initial.ints)
-        var changed = true
-        while (changed) {
-            changed = false
-            for (v in 0 until numBoolVars) {
-                if (cancellation()) return PropagationResult.Implied(bools, ints)
-                if (v in bools) continue
-                val tryTrue = propagate(Assumptions(bools + (v to true), ints), cancellation)
-                if (tryTrue is PropagationResult.Unsat) {
-                    val r = propagate(Assumptions(bools + (v to false), ints), cancellation)
-                    if (r is PropagationResult.Unsat) return r
-                    foldInto(bools, ints, v, false, r as PropagationResult.Implied)
-                    changed = true
-                    continue
-                }
-                val tryFalse = propagate(Assumptions(bools + (v to false), ints), cancellation)
-                if (tryFalse is PropagationResult.Unsat) {
-                    val r = propagate(Assumptions(bools + (v to true), ints), cancellation)
-                    if (r is PropagationResult.Unsat) return r
-                    foldInto(bools, ints, v, true, r as PropagationResult.Implied)
-                    changed = true
-                }
-            }
-        }
-        return PropagationResult.Implied(bools, ints)
-    }
+        // The common no-probe case seeds the shared empty sentinel — return the base bake untouched.
+        // A non-sentinel seed can carry bound tightenings / holes with no pins, so `isEmpty` (which only
+        // inspects pins) is not a safe skip: merge unconditionally.
+        seed === PropagationResult.Implied.EMPTY -> base
 
-    private fun foldInto(
-        bools: HashMap<Int, Boolean>,
-        ints: HashMap<Int, Int>,
-        forcedVar: Int,
-        forcedValue: Boolean,
-        implied: PropagationResult.Implied,
-    ) {
-        bools[forcedVar] = forcedValue
-        implied.forEachBool { k, b -> bools[k] = b }
-        implied.forEachInt { k, i -> ints[k] = i }
+        else -> (base as PropagationResult.Implied).merge(seed as PropagationResult.Implied)
     }
 
     /**
diff --git a/klause/src/commonMain/kotlin/com/eignex/klause/solver/result/SatisfyResult.kt b/klause/src/commonMain/kotlin/com/eignex/klause/solver/result/SatisfyResult.kt
index 28752ef78..6d43b42ea 100644
--- a/klause/src/commonMain/kotlin/com/eignex/klause/solver/result/SatisfyResult.kt
+++ b/klause/src/commonMain/kotlin/com/eignex/klause/solver/result/SatisfyResult.kt
@@ -111,11 +111,12 @@ private fun satisfyUnderAssumptionsBacktrack(
         }
     }
     val problem = solver.problem
-    if (problem.baked is PropagationResult.Unsat) {
-        val core = if (problem.baked.conflictFactors.isEmpty()) {
+    val baked = problem.baked
+    if (baked is PropagationResult.Unsat) {
+        val core = if (baked.conflictFactors.isEmpty()) {
             null
         } else {
-            UnsatCore.of(problem.baked.conflictFactors)
+            UnsatCore.of(baked.conflictFactors)
         }
         return SatisfyResult.GloballyUnsat(core)
     }
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/backtrack/lp/LpHarvestTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/backtrack/lp/LpHarvestTest.kt
index 18ba8b1b5..94753d316 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/backtrack/lp/LpHarvestTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/backtrack/lp/LpHarvestTest.kt
@@ -59,7 +59,7 @@ class LpHarvestTest {
             }
             val problem = Problem(0, n, domains, factors.toTypedArray())
             val obj = LinearObjective(intCoefficients = LongArray(n) { 1L })
-            val harvested = lpHarvest(problem, obj, shavingParams, Cancellation.Never)
+            val harvested = lpHarvest(problem, obj, shavingParams, cancellation = Cancellation.Never)
             if (harvested === problem) return@repeat
             engaged++
             // Every assignment feasible under the original constraints must still lie inside the
@@ -115,7 +115,7 @@ class LpHarvestTest {
             ),
         )
         val obj = LinearObjective(intCoefficients = longArrayOf(0L, 0L, 0L, 1L))
-        val harvested = lpHarvest(problem, obj, objShavingParams, Cancellation.Never)
+        val harvested = lpHarvest(problem, obj, objShavingParams, cancellation = Cancellation.Never)
         assertTrue(harvested !== problem, "objective shaving proved a floor; the harvest must apply it")
         assertTrue(harvested.intDomains[3].min >= 2, "objective floor z>=2 not folded into the domain")
         assertTrue(2 in harvested.intDomains[3], "harvest excluded the attainable optimum z=2")
@@ -134,7 +134,7 @@ class LpHarvestTest {
         val obj = LinearObjective(intCoefficients = longArrayOf(0L, -1L))
         assertSame(
             problem,
-            lpHarvest(problem, obj, objShavingParams, Cancellation.Never),
+            lpHarvest(problem, obj, objShavingParams, cancellation = Cancellation.Never),
             "a maximised objective yields no ascending floor, so the harvest is unchanged",
         )
     }
@@ -152,7 +152,7 @@ class LpHarvestTest {
             ),
         )
         val obj = LinearObjective(intCoefficients = longArrayOf(1L, 1L))
-        val harvested = lpHarvest(problem, obj, shavingParams, Cancellation.Never)
+        val harvested = lpHarvest(problem, obj, shavingParams, cancellation = Cancellation.Never)
         for (v in 0 until problem.numIntVars) {
             assertTrue(harvested.intDomains[v].min >= problem.intDomains[v].min, "lower bound widened for x$v")
             assertTrue(harvested.intDomains[v].max <= problem.intDomains[v].max, "upper bound widened for x$v")
@@ -176,7 +176,7 @@ class LpHarvestTest {
             ),
         )
         assertTrue(problem.baked !is PropagationResult.Unsat, "propagation alone must not catch this infeasibility")
-        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, Cancellation.Never)
+        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, cancellation = Cancellation.Never)
         assertTrue(harvested.baked is PropagationResult.Unsat, "the LP-certified infeasibility must bake to Unsat")
     }
 
@@ -196,7 +196,7 @@ class LpHarvestTest {
                 Linear(intArrayOf(1, 1, 1), intArrayOf(0, 1, 2), LinearOp.LE, 5), // implied by the three above
             ),
         )
-        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, Cancellation.Never)
+        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, cancellation = Cancellation.Never)
         assertTrue(harvested.factors.none { it is Linear && it.vars.size == 3 }, "the implied x+y+z<=5 must be dropped")
         assertEquals(3, harvested.factors.count { it is Linear }, "the three irredundant pairwise covers stay")
         assertSameFeasibleSet(problem, harvested, hi = 10)
@@ -218,7 +218,7 @@ class LpHarvestTest {
                 Linear(intArrayOf(1, 1, 1), intArrayOf(0, 1, 2), LinearOp.GE, 4), // implied by the three above
             ),
         )
-        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, Cancellation.Never)
+        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, cancellation = Cancellation.Never)
         assertTrue(harvested.factors.none { it is Linear && it.vars.size == 3 }, "the implied x+y+z>=4 must be dropped")
         assertEquals(3, harvested.factors.count { it is Linear }, "the three irredundant pairwise covers stay")
         assertSameFeasibleSet(problem, harvested, hi = 10)
@@ -239,7 +239,7 @@ class LpHarvestTest {
                 Linear(intArrayOf(1, -1), intArrayOf(2, 0), LinearOp.LE, 0), // z - x <= 0
             ),
         )
-        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, Cancellation.Never)
+        val harvested = lpHarvest(problem, LinearObjective(), shavingParams, cancellation = Cancellation.Never)
         assertTrue(
             harvested.factors.any { it is Linear && it.op == LinearOp.EQ && it.vars.size == 2 },
             "the LP-pinned difference must be added as a two-term equality",
@@ -262,7 +262,12 @@ class LpHarvestTest {
                 Linear(intArrayOf(1, 1, 1), intArrayOf(0, 1, 2), LinearOp.LE, 5),
             ),
         )
-        val report = lpHarvestReporting(problem, LinearObjective(), shavingParams, Cancellation.Never).report
+        val report = lpHarvestReporting(
+            problem,
+            LinearObjective(),
+            shavingParams,
+            cancellation = Cancellation.Never,
+        ).report
         assertEquals(1, report.constraintsRemoved, "the LP-redundant row must be counted")
         assertTrue(!report.rootInfeasible && report.equalitiesAdded == 0, "no other LP action fired here")
         assertTrue(!report.skipped && report.relaxationNnz > 0, "the built relaxation's size must be reported")
@@ -282,7 +287,12 @@ class LpHarvestTest {
                 Linear(intArrayOf(1, 1, 1), intArrayOf(0, 1, 2), LinearOp.LE, 4),
             ),
         )
-        val report = lpHarvestReporting(problem, LinearObjective(), shavingParams, Cancellation.Never).report
+        val report = lpHarvestReporting(
+            problem,
+            LinearObjective(),
+            shavingParams,
+            cancellation = Cancellation.Never,
+        ).report
         assertTrue(report.rootInfeasible, "root-LP infeasibility must be recorded in the report")
     }
 
@@ -301,7 +311,7 @@ class LpHarvestTest {
                 factors.add(Linear(coeffs, IntArray(n) { it }, LinearOp.LE, rng.nextInt(0, hi * n + 1)))
             }
             val problem = Problem(0, n, domains, factors.toTypedArray())
-            val harvested = lpHarvest(problem, LinearObjective(), shavingParams, Cancellation.Never)
+            val harvested = lpHarvest(problem, LinearObjective(), shavingParams, cancellation = Cancellation.Never)
             if (harvested.factors.size < problem.factors.size) dropped++
             assertSameFeasibleSet(problem, harvested, hi)
         }
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/factor/symmetry/SymmetryPropagatorTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/factor/symmetry/SymmetryPropagatorTest.kt
index a92b164f1..bcd42a230 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/factor/symmetry/SymmetryPropagatorTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/factor/symmetry/SymmetryPropagatorTest.kt
@@ -10,7 +10,9 @@ import com.eignex.klause.factor.arithmetic.ReifiedLinear
 import com.eignex.klause.factor.bool.PseudoBoolean
 import com.eignex.klause.factor.global.AllDifferent
 import com.eignex.klause.model.PbOp
+import com.eignex.klause.presolve.BakeConfig
 import com.eignex.klause.presolve.Presolve
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.solver.Factor
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Lit
@@ -36,7 +38,7 @@ class SymmetryPropagatorTest {
     private fun key(s: Sample) = s.bools.toList() to s.ints.toList()
 
     private fun assertSoundUnderSearch(name: String, problem: Problem) {
-        val broken = Presolve.breakSymmetries(problem)
+        val broken = problem.withPassDelta(Presolve.breakSymmetries(problem), BakeConfig.NONE)
         val original = BruteForceSolver(
             problem,
         ).enumerate(BruteForceParams(randomSeed = 0L)).map { key(it) }.toHashSet()
@@ -118,7 +120,7 @@ class SymmetryPropagatorTest {
                 }
             }
             val problem = Problem(0, n, Array(n) { IntDomain(0, d) }, factors)
-            val broken = Presolve.breakSymmetries(problem)
+            val broken = problem.withPassDelta(Presolve.breakSymmetries(problem), BakeConfig.NONE)
             val origSat = BruteForceSolver(problem).solve(BruteForceParams(randomSeed = 0L)) is SolveResult.Sat
             val brokenSat = BacktrackSolver(broken).solve(BacktrackParams(randomSeed = 1L)) is SolveResult.Sat
             assertEquals(origSat, brokenSat, "random#$iter(n=$n,d=$d): breaking changed satisfiability")
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/AffineEliminationTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/AffineEliminationTest.kt
index cfb24124b..9bea085a5 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/AffineEliminationTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/AffineEliminationTest.kt
@@ -7,6 +7,7 @@ import com.eignex.klause.factor.arithmetic.LinearOp
 import com.eignex.klause.factor.global.AllDifferent
 import com.eignex.klause.factor.table.Element
 import com.eignex.klause.factor.table.Table
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.IntDomain
@@ -35,14 +36,16 @@ class AffineEliminationTest {
         BacktrackSolver(problem).solve(BacktrackParams()) is SolveResult.Sat
 
     private fun checkRoundTrip(name: String, original: Problem, expectEliminated: Boolean, expectSat: Boolean) {
-        val elim = Presolve.eliminateAffineSingletons(original)
-        assertEquals(expectEliminated, elim.problem !== original, "$name: elimination expectation wrong")
+        val delta = Presolve.eliminateAffineSingletons(original)
+        assertEquals(expectEliminated, !delta.isEmpty, "$name: elimination expectation wrong")
+        val reduced = original.withPassDelta(delta, BakeConfig.NONE)
+        val reconstruct = delta.reconstruct ?: { it }
         assertEquals(expectSat, verdictSat(original), "$name: original verdict unexpected")
-        assertEquals(verdictSat(original), verdictSat(elim.problem), "$name: verdict changed by elimination")
-        if (verdictSat(elim.problem)) {
-            val reduced = BacktrackSolver(elim.problem).solve(BacktrackParams())
-            check(reduced is SolveResult.Sat)
-            val full = elim.reconstruct(reduced.assignment)
+        assertEquals(verdictSat(original), verdictSat(reduced), "$name: verdict changed by elimination")
+        if (verdictSat(reduced)) {
+            val solved = BacktrackSolver(reduced).solve(BacktrackParams())
+            check(solved is SolveResult.Sat)
+            val full = reconstruct(solved.assignment)
             assertTrue(isFeasible(original, full), "$name: reconstructed sample infeasible in original")
         }
     }
@@ -51,13 +54,15 @@ class AffineEliminationTest {
      *  to a feasible assignment of the original, and the reconstructed set is *exactly* the original's
      *  feasible set (no solution lost, none invented). Small domains only — full enumeration. */
     private fun checkFeasibleSetPreserved(name: String, original: Problem) {
-        val elim = Presolve.eliminateAffineSingletons(original)
-        assertTrue(elim.problem !== original, "$name: expected an elimination")
+        val delta = Presolve.eliminateAffineSingletons(original)
+        assertTrue(!delta.isEmpty, "$name: expected an elimination")
+        val reduced = original.withPassDelta(delta, BakeConfig.NONE)
+        val reconstruct = delta.reconstruct ?: { it }
         val origFeasible = feasibleSet(original)
         val reconstructed = HashSet<List<Int>>()
-        enumerate(elim.problem.intDomains) { assign ->
-            if (isFeasible(elim.problem, Sample(BooleanArray(0), assign))) {
-                val full = elim.reconstruct(Sample(BooleanArray(0), assign.copyOf()))
+        enumerate(reduced.intDomains) { assign ->
+            if (isFeasible(reduced, Sample(BooleanArray(0), assign))) {
+                val full = reconstruct(Sample(BooleanArray(0), assign.copyOf()))
                 assertTrue(isFeasible(original, full), "$name: reconstructed $full infeasible in original")
                 reconstructed.add(full.ints.toList())
             }
@@ -353,8 +358,8 @@ class AffineEliminationTest {
             intDomains = arrayOf(IntDomain(0, 20), IntDomain(0, 3), IntDomain(0, 3)),
             factors = listOf(Linear(intArrayOf(2, -4, -6), intArrayOf(0, 1, 2), LinearOp.EQ, 8)),
         )
-        val elim = Presolve.eliminateAffineSingletons(problem, objectiveIntVars = setOf(0))
-        assertTrue(elim.problem === problem, "objective-protected: must not eliminate x0")
+        val delta = Presolve.eliminateAffineSingletons(problem, objectiveIntVars = setOf(0))
+        assertTrue(delta.isEmpty, "objective-protected: must not eliminate x0")
     }
 
     @Test
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/CoefficientStrengtheningTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/CoefficientStrengtheningTest.kt
index ddb3678d1..2058991ad 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/CoefficientStrengtheningTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/CoefficientStrengtheningTest.kt
@@ -4,6 +4,7 @@ import com.eignex.klause.factor.arithmetic.Linear
 import com.eignex.klause.factor.arithmetic.LinearOp
 import com.eignex.klause.factor.bool.PseudoBoolean
 import com.eignex.klause.model.PbOp
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.IntDomain
@@ -21,13 +22,16 @@ import kotlin.test.assertTrue
  */
 class CoefficientStrengtheningTest {
 
+    private fun strengthened(problem: Problem): Problem =
+        problem.withPassDelta(Presolve.strengthenCoefficients(problem), BakeConfig.NONE)
+
     @Test
     fun `coefficient lifting is probing-informed - SAC-tightened bounds give a tighter lift`() {
         // The lift target 2*x0 + 5*x2 <= 8 with x0 in [0,3], x2 in [0,1]: its lift clamps coefficients
         // to d = (max activity) - bound. SAC probing tightens x0's upper bound, shrinking the activity
         // and so the clamp — i.e. lifting reads the *baked* (probed) domains, not the declared ones.
         fun strengthenedTarget(probe: Boolean): Linear {
-            val p = Problem(
+            val base = Problem(
                 numBoolVars = 0,
                 numIntVars = 3,
                 intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3), IntDomain(0, 1)),
@@ -36,9 +40,9 @@ class CoefficientStrengtheningTest {
                     Linear(intArrayOf(1, 1), intArrayOf(0, 1), LinearOp.LE, 4), // x0 + x1 <= 4 (SAC: x0 <= 2)
                     Linear(intArrayOf(2, 5), intArrayOf(0, 2), LinearOp.LE, 8), // lift target
                 ),
-                probeIntBounds = probe,
             )
-            val out = Presolve.strengthenCoefficients(p)
+            val p = RootBaker.reseed(base, BakeConfig(probeIntBounds = probe))
+            val out = strengthened(p)
             return out.factors.filterIsInstance<Linear>().single { 0 in it.vars && 2 in it.vars }
         }
         // Probing off: root propagation leaves x0 in [0,3] ⇒ d = 2*3 + 5*1 - 8 = 3, x2's 5 clamps to 3.
@@ -89,7 +93,7 @@ class CoefficientStrengtheningTest {
         // The rewrite may produce one factor (lifted / gcd-reduced), none (dropped ⇒ always-true), or
         // a multi-factor contradiction (an indivisible equality ⇒ infeasible); the feasible set is the
         // conjunction of whatever rewritten factors remain.
-        val rewritten = Presolve.strengthenCoefficients(problem).factors.filterIsInstance<Linear>()
+        val rewritten = strengthened(problem).factors.filterIsInstance<Linear>()
         val values = Array(numVars) { v ->
             val d = problem.intDomains[v]
             IntArray(d.size) { d.valueAt(it) }
@@ -123,7 +127,7 @@ class CoefficientStrengtheningTest {
 
     private fun assertPbEquivalent(numVars: Int, original: PseudoBoolean) {
         val problem = Problem(numVars, 0, emptyArray(), listOf(original))
-        val rewritten = Presolve.strengthenCoefficients(problem).factors.getOrNull(0) as? PseudoBoolean
+        val rewritten = strengthened(problem).factors.getOrNull(0) as? PseudoBoolean
         val bools = BooleanArray(numVars)
         for (mask in 0 until (1 shl numVars)) {
             for (v in 0 until numVars) bools[v] = (mask shr v) and 1 == 1
@@ -144,7 +148,7 @@ class CoefficientStrengtheningTest {
     }
 
     private fun assertInfeasibleAfterStrengthen(problem: Problem) {
-        val out = Presolve.strengthenCoefficients(problem)
+        val out = strengthened(problem)
         assertTrue(
             out.propagate(Assumptions.None) is PropagationResult.Unsat,
             "strengthened problem should be infeasible: ${out.factors}",
@@ -176,7 +180,7 @@ class CoefficientStrengtheningTest {
     @Test
     fun `a divisible equality is not flagged infeasible`() {
         // 2*x0 + 4*x1 = 6 divides through cleanly and stays satisfiable (x0=1, x1=1).
-        val out = Presolve.strengthenCoefficients(
+        val out = strengthened(
             Problem(
                 0,
                 2,
@@ -303,7 +307,7 @@ class CoefficientStrengtheningTest {
         // d = Amax − b = 4 (so no lifting), and not so loose the bound tightens the [0,2] domains.
         val original = Linear(intArrayOf(2, 3), intArrayOf(0, 1), LinearOp.LE, 6)
         val problem = Problem(0, 2, Array(2) { IntDomain(0, 2) }, listOf(original))
-        assertTrue(Presolve.strengthenCoefficients(problem).factors[0] === original, "coprime factor was rewritten")
+        assertTrue(strengthened(problem).factors[0] === original, "coprime factor was rewritten")
     }
 
     @Test
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DominatedVariablesTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DominatedVariablesTest.kt
index e8f35a319..48b473885 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DominatedVariablesTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DominatedVariablesTest.kt
@@ -7,6 +7,7 @@ import com.eignex.klause.factor.bool.Clause
 import com.eignex.klause.factor.bool.PseudoBoolean
 import com.eignex.klause.factor.global.AllDifferent
 import com.eignex.klause.model.PbOp
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.IntDomain
@@ -14,7 +15,6 @@ import com.eignex.klause.solver.Lit
 import com.eignex.klause.solver.Problem
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 /**
@@ -53,13 +53,18 @@ class DominatedVariablesTest {
         return best
     }
 
+    private fun fixed(problem: Problem, intCoeffs: Map<Int, Long>, boolCoeffs: Map<Int, Long> = emptyMap()): Problem =
+        problem.withPassDelta(Presolve.fixDominatedVariables(problem, intCoeffs, boolCoeffs), BakeConfig.NONE)
+
     private fun checkDualFix(name: String, problem: Problem, coeffs: Map<Int, Long>, expectFixed: Set<Int>) {
-        val out = Presolve.fixDominatedVariables(problem, coeffs)
+        val out = fixed(problem, coeffs)
         assertEquals(minObjective(problem, coeffs), minObjective(out, coeffs), "$name: optimum changed")
         for (v in expectFixed) {
             assertTrue(out.intDomains[v].min == out.intDomains[v].max, "$name: var $v should be pinned")
         }
-        if (expectFixed.isEmpty()) assertSame(problem, out, "$name: expected no fixing")
+        if (expectFixed.isEmpty()) {
+            assertTrue(Presolve.fixDominatedVariables(problem, coeffs).isEmpty, "$name: expected no fixing")
+        }
     }
 
     @Test
@@ -73,7 +78,7 @@ class DominatedVariablesTest {
             listOf(Linear(intArrayOf(1, 1), intArrayOf(0, 1), LinearOp.LE, 3)),
         )
         checkDualFix("down-safe", problem, emptyMap(), setOf(0, 1))
-        val out = Presolve.fixDominatedVariables(problem, emptyMap())
+        val out = fixed(problem, emptyMap())
         assertEquals(0, out.intDomains[0].min)
         assertEquals(0, out.intDomains[0].max)
     }
@@ -100,7 +105,7 @@ class DominatedVariablesTest {
             Array(2) { IntDomain(0, 5) },
             listOf(Linear(intArrayOf(-1, 1), intArrayOf(0, 1), LinearOp.LE, 4)),
         )
-        val out = Presolve.fixDominatedVariables(problem, mapOf(0 to -1L))
+        val out = fixed(problem, mapOf(0 to -1L))
         assertEquals(minObjective(problem, mapOf(0 to -1L)), minObjective(out, mapOf(0 to -1L)), "optimum changed")
         assertEquals(5, out.intDomains[0].min)
         assertEquals(5, out.intDomains[0].max)
@@ -120,7 +125,7 @@ class DominatedVariablesTest {
                 Linear(intArrayOf(1, 1), intArrayOf(0, 2), LinearOp.GE, 2),
             ),
         )
-        val out = Presolve.fixDominatedVariables(problem, emptyMap())
+        val out = fixed(problem, emptyMap())
         assertEquals(minObjective(problem, emptyMap()), minObjective(out, emptyMap()), "optimum changed")
         assertTrue(out.intDomains[0].min != out.intDomains[0].max, "x0 must stay free")
     }
@@ -165,7 +170,7 @@ class DominatedVariablesTest {
         // b0, b1 appear only positively (in a single clause) ⇒ setting them true satisfies it and is
         // always safe ⇒ both pinned true with a unit clause; the optimum (no objective) is preserved.
         val problem = Problem(2, 0, emptyArray(), listOf(Clause(intArrayOf(pos(0), pos(1)))))
-        val out = Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap())
+        val out = fixed(problem, emptyMap(), emptyMap())
         assertEquals(minObjectiveBools(problem, emptyMap()), minObjectiveBools(out, emptyMap()), "optimum changed")
         assertTrue(hasUnit(out, Lit.make(0, true)), "b0 should be pinned true")
         assertTrue(hasUnit(out, Lit.make(1, true)), "b1 should be pinned true")
@@ -177,7 +182,7 @@ class DominatedVariablesTest {
         // ⇒ it cannot be pinned either way. b1 (zero cost) is still pinned true.
         val problem = Problem(2, 0, emptyArray(), listOf(Clause(intArrayOf(pos(0), pos(1)))))
         val coeffs = mapOf(0 to 2L)
-        val out = Presolve.fixDominatedVariables(problem, emptyMap(), coeffs)
+        val out = fixed(problem, emptyMap(), coeffs)
         assertEquals(minObjectiveBools(problem, coeffs), minObjectiveBools(out, coeffs), "optimum changed")
         assertTrue(!hasUnit(out, Lit.make(0, true)) && !hasUnit(out, Lit.make(0, false)), "b0 must stay free")
     }
@@ -187,7 +192,7 @@ class DominatedVariablesTest {
         // c0 = −1 (true is beneficial) and true is safe ⇒ pin b0 true.
         val problem = Problem(2, 0, emptyArray(), listOf(Clause(intArrayOf(pos(0), pos(1)))))
         val coeffs = mapOf(0 to -1L)
-        val out = Presolve.fixDominatedVariables(problem, emptyMap(), coeffs)
+        val out = fixed(problem, emptyMap(), coeffs)
         assertEquals(minObjectiveBools(problem, coeffs), minObjectiveBools(out, coeffs), "optimum changed")
         assertTrue(hasUnit(out, Lit.make(0, true)), "b0 should be pinned true")
     }
@@ -202,7 +207,10 @@ class DominatedVariablesTest {
             emptyArray(),
             listOf(Cardinality(intArrayOf(pos(0), pos(1), pos(2)), min = 1, max = 1)),
         )
-        assertSame(problem, Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap()), "expected no fixing")
+        assertTrue(
+            Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap()).isEmpty,
+            "expected no fixing",
+        )
     }
 
     @Test
@@ -215,7 +223,7 @@ class DominatedVariablesTest {
             emptyArray(),
             listOf(Cardinality(intArrayOf(pos(0), pos(1), pos(2)), min = 1, max = 3)),
         )
-        val out = Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap())
+        val out = fixed(problem, emptyMap(), emptyMap())
         assertEquals(minObjectiveBools(problem, emptyMap()), minObjectiveBools(out, emptyMap()), "optimum changed")
         for (b in 0..2) assertTrue(hasUnit(out, Lit.make(b, true)), "b$b should be pinned true")
     }
@@ -230,7 +238,7 @@ class DominatedVariablesTest {
             emptyArray(),
             listOf(Cardinality(intArrayOf(pos(0), pos(1), pos(2)), min = 0, max = 1)),
         )
-        val out = Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap())
+        val out = fixed(problem, emptyMap(), emptyMap())
         assertEquals(minObjectiveBools(problem, emptyMap()), minObjectiveBools(out, emptyMap()), "optimum changed")
         for (b in 0..2) assertTrue(hasUnit(out, Lit.make(b, false)), "b$b should be pinned false")
     }
@@ -244,7 +252,7 @@ class DominatedVariablesTest {
             emptyArray(),
             listOf(PseudoBoolean(intArrayOf(2, 3), intArrayOf(pos(0), pos(1)), PbOp.LE, 4)),
         )
-        val outLe = Presolve.fixDominatedVariables(le, emptyMap(), emptyMap())
+        val outLe = fixed(le, emptyMap(), emptyMap())
         assertEquals(minObjectiveBools(le, emptyMap()), minObjectiveBools(outLe, emptyMap()), "LE optimum changed")
         assertTrue(hasUnit(outLe, Lit.make(0, false)) && hasUnit(outLe, Lit.make(1, false)), "LE bools pinned false")
     }
@@ -258,7 +266,7 @@ class DominatedVariablesTest {
             emptyArray(),
             listOf(PseudoBoolean(intArrayOf(2, 3), intArrayOf(pos(0), pos(1)), PbOp.GE, 1)),
         )
-        val outGe = Presolve.fixDominatedVariables(ge, emptyMap(), emptyMap())
+        val outGe = fixed(ge, emptyMap(), emptyMap())
         assertEquals(minObjectiveBools(ge, emptyMap()), minObjectiveBools(outGe, emptyMap()), "GE optimum changed")
         assertTrue(hasUnit(outGe, Lit.make(0, true)) && hasUnit(outGe, Lit.make(1, true)), "GE bools pinned true")
     }
@@ -268,7 +276,7 @@ class DominatedVariablesTest {
         // `-b0 <= 0` (always true): a rising sum violates LE, and with weight -1 the rising value is
         // b0 = false ⇒ false-unsafe ⇒ the safe pin is true. Optimum (no objective) is preserved.
         val problem = Problem(1, 0, emptyArray(), listOf(PseudoBoolean(intArrayOf(-1), intArrayOf(pos(0)), PbOp.LE, 0)))
-        val out = Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap())
+        val out = fixed(problem, emptyMap(), emptyMap())
         assertEquals(minObjectiveBools(problem, emptyMap()), minObjectiveBools(out, emptyMap()), "optimum changed")
         assertTrue(hasUnit(out, Lit.make(0, true)), "b0 should be pinned true")
     }
@@ -282,6 +290,9 @@ class DominatedVariablesTest {
             emptyArray(),
             listOf(PseudoBoolean(intArrayOf(1, 1), intArrayOf(pos(0), pos(1)), PbOp.EQ, 1)),
         )
-        assertSame(problem, Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap()), "expected no fixing")
+        assertTrue(
+            Presolve.fixDominatedVariables(problem, emptyMap(), emptyMap()).isEmpty,
+            "expected no fixing",
+        )
     }
 }
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DuplicateColumnsTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DuplicateColumnsTest.kt
index a5a2b631b..856a940e5 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DuplicateColumnsTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/DuplicateColumnsTest.kt
@@ -5,6 +5,7 @@ import com.eignex.klause.backtrack.BacktrackSolver
 import com.eignex.klause.factor.arithmetic.Linear
 import com.eignex.klause.factor.arithmetic.LinearOp
 import com.eignex.klause.factor.global.AllDifferent
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.IntDomain
@@ -13,7 +14,6 @@ import com.eignex.klause.solver.Sample
 import com.eignex.klause.solver.SolveResult
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 /**
@@ -35,14 +35,16 @@ class DuplicateColumnsTest {
         BacktrackSolver(problem).solve(BacktrackParams()) is SolveResult.Sat
 
     private fun checkRoundTrip(name: String, original: Problem, expectMerged: Boolean, expectSat: Boolean) {
-        val merge = Presolve.mergeDuplicateColumns(original)
-        assertEquals(expectMerged, merge.problem !== original, "$name: merge expectation wrong")
+        val delta = Presolve.mergeDuplicateColumns(original)
+        assertEquals(expectMerged, !delta.isEmpty, "$name: merge expectation wrong")
+        val reduced = original.withPassDelta(delta, BakeConfig.NONE)
+        val reconstruct = delta.reconstruct ?: { it }
         assertEquals(expectSat, verdictSat(original), "$name: original verdict unexpected")
-        assertEquals(verdictSat(original), verdictSat(merge.problem), "$name: verdict changed by merge")
-        if (verdictSat(merge.problem)) {
-            val reduced = BacktrackSolver(merge.problem).solve(BacktrackParams())
-            check(reduced is SolveResult.Sat)
-            val full = merge.reconstruct(reduced.assignment)
+        assertEquals(verdictSat(original), verdictSat(reduced), "$name: verdict changed by merge")
+        if (verdictSat(reduced)) {
+            val solved = BacktrackSolver(reduced).solve(BacktrackParams())
+            check(solved is SolveResult.Sat)
+            val full = reconstruct(solved.assignment)
             assertTrue(isFeasible(original, full), "$name: reconstructed sample infeasible in original")
         }
     }
@@ -52,13 +54,15 @@ class DuplicateColumnsTest {
      *  not recover *every* original solution — see `preservesSolutionSet = false`), and the reduced
      *  problem is feasible exactly when the original is. Small domains only — full enumeration. */
     private fun checkAllReconstructionsFeasible(name: String, original: Problem) {
-        val merge = Presolve.mergeDuplicateColumns(original)
-        assertTrue(merge.problem !== original, "$name: expected a merge")
+        val delta = Presolve.mergeDuplicateColumns(original)
+        assertTrue(!delta.isEmpty, "$name: expected a merge")
+        val reduced = original.withPassDelta(delta, BakeConfig.NONE)
+        val reconstruct = delta.reconstruct ?: { it }
         var anyReduced = false
-        enumerate(merge.problem.intDomains) { assign ->
-            if (isFeasible(merge.problem, Sample(BooleanArray(0), assign))) {
+        enumerate(reduced.intDomains) { assign ->
+            if (isFeasible(reduced, Sample(BooleanArray(0), assign))) {
                 anyReduced = true
-                val full = merge.reconstruct(Sample(BooleanArray(0), assign.copyOf()))
+                val full = reconstruct(Sample(BooleanArray(0), assign.copyOf()))
                 assertTrue(isFeasible(original, full), "$name: reconstructed $full infeasible in original")
             }
         }
@@ -105,10 +109,10 @@ class DuplicateColumnsTest {
                 Linear(intArrayOf(1, 1), intArrayOf(0, 1), LinearOp.GE, 1),
             ),
         )
-        val merge = Presolve.mergeDuplicateColumns(problem)
-        assertTrue(merge.problem !== problem, "expected a merge")
+        val reduced = problem.withPassDelta(Presolve.mergeDuplicateColumns(problem), BakeConfig.NONE)
+        assertTrue(reduced !== problem, "expected a merge")
         assertTrue(
-            merge.problem.factors.none { 1 in it.intVars },
+            reduced.factors.none { 1 in it.intVars },
             "the dropped duplicate column is absorbed and appears in no factor",
         )
         checkAllReconstructionsFeasible("exact-duplicate", problem)
@@ -143,8 +147,8 @@ class DuplicateColumnsTest {
                 Linear(intArrayOf(1, 1), intArrayOf(0, 1), LinearOp.GE, 1),
             ),
         )
-        val merge = DuplicateColumns.mergeDuplicateColumns(problem, objectiveIntVars = setOf(1))
-        assertSame(problem, merge.problem, "an objective variable must not be merged")
+        val delta = DuplicateColumns.mergeDuplicateColumns(problem, objectiveIntVars = setOf(1))
+        assertTrue(delta.isEmpty, "an objective variable must not be merged")
     }
 
     @Test
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ImplicationGraphTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ImplicationGraphTest.kt
index ec36b03ed..864553f98 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ImplicationGraphTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ImplicationGraphTest.kt
@@ -3,6 +3,7 @@ package com.eignex.klause.presolve
 import com.eignex.klause.backtrack.BacktrackParams
 import com.eignex.klause.backtrack.BacktrackSolver
 import com.eignex.klause.factor.bool.Clause
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.Lit
@@ -11,7 +12,6 @@ import com.eignex.klause.solver.Sample
 import com.eignex.klause.solver.SolveResult
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 /**
@@ -34,11 +34,17 @@ class ImplicationGraphTest {
     private fun binaryCount(problem: Problem): Int =
         problem.factors.filterIsInstance<Clause>().count { it.literals.size == 2 }
 
-    /** Solve the reduced problem, reconstruct, and assert the lifted sample is feasible in [original]. */
-    private fun assertRoundTrip(original: Problem, reduction: ImplicationReduction) {
-        val solved = BacktrackSolver(reduction.problem).solve(BacktrackParams())
+    /** The problem [Presolve.reduceImplicationGraph] reduces [problem] to, materialized from its delta. */
+    private fun reduced(problem: Problem, objectiveBoolVars: Set<Int> = emptySet()): Problem {
+        val delta = Presolve.reduceImplicationGraph(problem, cap, objectiveBoolVars = objectiveBoolVars)
+        return problem.withPassDelta(delta, BakeConfig.NONE)
+    }
+
+    /** Solve the reduced problem, reconstruct via the [delta], and assert the lifted sample is feasible. */
+    private fun assertRoundTrip(original: Problem, delta: PassDelta) {
+        val solved = BacktrackSolver(original.withPassDelta(delta, BakeConfig.NONE)).solve(BacktrackParams())
         check(solved is SolveResult.Sat) { "reduced problem should be satisfiable" }
-        val full = reduction.reconstruct(solved.assignment)
+        val full = (delta.reconstruct ?: { it })(solved.assignment)
         assertTrue(isFeasible(original, full), "reconstructed sample infeasible in the original")
     }
 
@@ -55,9 +61,8 @@ class ImplicationGraphTest {
                 Clause(intArrayOf(Lit.make(1, false), Lit.make(0, true))),
             ),
         )
-        val reduction = Presolve.reduceImplicationGraph(problem, cap)
-        assertTrue(reduction.problem.factors.none { 1 in it.boolVars }, "b1 should be substituted away")
-        assertRoundTrip(problem, reduction)
+        assertTrue(reduced(problem).factors.none { 1 in it.boolVars }, "b1 should be substituted away")
+        assertRoundTrip(problem, Presolve.reduceImplicationGraph(problem, cap))
     }
 
     @Test
@@ -75,9 +80,8 @@ class ImplicationGraphTest {
                 Clause(intArrayOf(Lit.make(2, false), Lit.make(1, true))),
             ),
         )
-        val reduction = Presolve.reduceImplicationGraph(problem, cap)
-        assertTrue(reduction.problem.factors.none { 1 in it.boolVars || 2 in it.boolVars }, "b1, b2 merged into b0")
-        assertRoundTrip(problem, reduction)
+        assertTrue(reduced(problem).factors.none { 1 in it.boolVars || 2 in it.boolVars }, "b1, b2 merged into b0")
+        assertRoundTrip(problem, Presolve.reduceImplicationGraph(problem, cap))
     }
 
     @Test
@@ -93,8 +97,7 @@ class ImplicationGraphTest {
                 Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true))),
             ),
         )
-        val reduction = Presolve.reduceImplicationGraph(problem, cap)
-        assertTrue(reduction.problem.factors.any { 1 in it.boolVars }, "anti-equivalent b1 must not be merged away")
+        assertTrue(reduced(problem).factors.any { 1 in it.boolVars }, "anti-equivalent b1 must not be merged away")
     }
 
     @Test
@@ -111,9 +114,8 @@ class ImplicationGraphTest {
                 Clause(intArrayOf(Lit.make(0, false), Lit.make(2, true))), // a -> c (redundant)
             ),
         )
-        val reduction = Presolve.reduceImplicationGraph(problem, cap)
-        assertEquals(2, binaryCount(reduction.problem), "the redundant a -> c binary is dropped")
-        assertRoundTrip(problem, reduction)
+        assertEquals(2, binaryCount(reduced(problem)), "the redundant a -> c binary is dropped")
+        assertRoundTrip(problem, Presolve.reduceImplicationGraph(problem, cap))
     }
 
     @Test
@@ -129,9 +131,8 @@ class ImplicationGraphTest {
                 Clause(intArrayOf(Lit.make(1, false), Lit.make(2, true))),
             ),
         )
-        val reduction = Presolve.reduceImplicationGraph(problem, cap)
-        assertEquals(2, binaryCount(reduction.problem), "no binary is redundant")
-        assertSame(problem, reduction.problem, "nothing to reduce is the pass's no-op signal")
+        assertEquals(2, binaryCount(reduced(problem)), "no binary is redundant")
+        assertTrue(Presolve.reduceImplicationGraph(problem, cap).isEmpty, "nothing to reduce is the no-op signal")
     }
 
     @Test
@@ -147,8 +148,10 @@ class ImplicationGraphTest {
                 Clause(intArrayOf(Lit.make(1, false), Lit.make(0, true))),
             ),
         )
-        val reduction = Presolve.reduceImplicationGraph(problem, cap, objectiveBoolVars = setOf(1))
-        assertTrue(reduction.problem.factors.any { 1 in it.boolVars }, "an objective variable must not be merged")
+        assertTrue(
+            reduced(problem, objectiveBoolVars = setOf(1)).factors.any { 1 in it.boolVars },
+            "an objective variable must not be merged",
+        )
     }
 
     @Test
@@ -161,7 +164,7 @@ class ImplicationGraphTest {
             intDomains = emptyArray(),
             factors = listOf(Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true)))),
         )
-        assertSame(problem, Presolve.reduceImplicationGraph(problem, cap).problem, "no reduction is the no-op signal")
+        assertTrue(Presolve.reduceImplicationGraph(problem, cap).isEmpty, "no reduction is the no-op signal")
     }
 
     @Test
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/PresolveSessionTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/PresolveSessionTest.kt
new file mode 100644
index 000000000..e5bb2ece1
--- /dev/null
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/PresolveSessionTest.kt
@@ -0,0 +1,80 @@
+package com.eignex.klause.presolve
+
+import com.eignex.klause.factor.arithmetic.Linear
+import com.eignex.klause.factor.arithmetic.LinearOp
+import com.eignex.klause.solver.Factor
+import com.eignex.klause.solver.IntDomain
+import com.eignex.klause.solver.Problem
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertFalse
+import kotlin.test.assertTrue
+
+/**
+ * [PresolveSession] applies pass deltas incrementally against one persistent [PropagationState] and
+ * materializes the solver [Problem] once at the end. Each test checks the incremental result against
+ * an independent one-shot [PresolveShared.rebuildProblem] over the same final factor set + narrowings —
+ * they must agree because the propagators are monotone (the greatest fixpoint is unique).
+ */
+class PresolveSessionTest {
+
+    private fun domains() = arrayOf(IntDomain(0, 10), IntDomain(0, 10), IntDomain(0, 10))
+
+    private fun leq(coeffs: IntArray, vars: IntArray, bound: Int) = Linear(coeffs, vars, LinearOp.LE, bound)
+
+    private fun base(vararg factors: Factor) = Problem(0, 3, domains(), factors.toList())
+
+    private fun bounds(problem: Problem) = (0 until problem.numIntVars).map {
+        problem.intDomains[it].min to
+            problem.intDomains[it].max
+    }
+
+    @Test
+    fun `dropping a redundant factor and adding one matches a one-shot build`() {
+        val f0 = leq(intArrayOf(1), intArrayOf(0), 5) // x0 <= 5
+        val f1 = leq(intArrayOf(1), intArrayOf(0), 7) // x0 <= 7, redundant given f0
+        val f2 = leq(intArrayOf(1, -1), intArrayOf(1, 0), 0) // x1 <= x0
+        val g = leq(intArrayOf(1, -1), intArrayOf(2, 1), 0) // x2 <= x1
+
+        val session = PresolveSession(base(f0, f1, f2))
+        assertTrue(session.apply(PresolveDelta(droppedIds = intArrayOf(1), addedFactors = listOf(g))))
+        val got = session.materialize()
+
+        val reference = PresolveShared.rebuildProblem(base(f0, f2, g), listOf(f0, f2, g), domains())
+        assertEquals(bounds(reference), bounds(got))
+        assertEquals(3, got.factors.size)
+        assertEquals(0 to 5, got.intDomains[2].min to got.intDomains[2].max) // x2 upper-bounded through the chain
+    }
+
+    @Test
+    fun `a pushed domain narrowing propagates and matches a one-shot build`() {
+        val f0 = leq(intArrayOf(1), intArrayOf(0), 5) // x0 <= 5
+        val f2 = leq(intArrayOf(1, -1), intArrayOf(1, 0), 0) // x1 <= x0
+        val g = leq(intArrayOf(1, -1), intArrayOf(2, 1), 0) // x2 <= x1
+
+        val session = PresolveSession(base(f0, f2))
+        assertTrue(session.apply(PresolveDelta(addedFactors = listOf(g))))
+        // A dual-fix-style direct narrowing: x0 <= 3, not implied by any factor.
+        val narrowed = arrayOf(IntDomain(0, 3), IntDomain(0, 10), IntDomain(0, 10))
+        assertTrue(session.apply(PresolveDelta(domains = narrowed)))
+        val got = session.materialize()
+
+        val reference = PresolveShared.rebuildProblem(
+            base(f0, f2, g),
+            listOf(f0, f2, g),
+            arrayOf(IntDomain(0, 3), IntDomain(0, 10), IntDomain(0, 10)),
+        )
+        assertEquals(bounds(reference), bounds(got))
+        assertEquals(0 to 3, got.intDomains[2].min to got.intDomains[2].max) // x2 upper-bounded through the chain
+    }
+
+    @Test
+    fun `a conflicting narrowing latches infeasibility`() {
+        val f0 = leq(intArrayOf(1), intArrayOf(0), 5) // x0 <= 5
+        val g = leq(intArrayOf(-1), intArrayOf(0), -8) // -x0 <= -8, i.e. x0 >= 8
+
+        val session = PresolveSession(base(f0))
+        assertFalse(session.apply(PresolveDelta(addedFactors = listOf(g)))) // 8 <= x0 <= 5 is infeasible
+        assertTrue(session.infeasible)
+    }
+}
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/PresolverTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/PresolverTest.kt
index be611a2f9..bf3c705e6 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/PresolverTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/PresolverTest.kt
@@ -8,6 +8,7 @@ import com.eignex.klause.factor.bool.Clause
 import com.eignex.klause.factor.bool.Xor
 import com.eignex.klause.factor.circuit.Circuit
 import com.eignex.klause.factor.global.AllDifferent
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.Factor
@@ -136,8 +137,8 @@ class PresolverTest {
             listOf(Linear(intArrayOf(1), intArrayOf(0), LinearOp.LE, 2)),
         )
         for (p in PresolvePass.entries.filter { it.stage == PresolvePass.Stage.PROBLEM }) {
-            val result = p.apply(trivial, PresolveContext.EMPTY)
-            assertEquals(trivial.numIntVars, result.problem.numIntVars, "${p.id} returned a malformed problem")
+            val applied = trivial.withPassDelta(p.apply(trivial, PresolveContext.EMPTY), BakeConfig.NONE)
+            assertEquals(trivial.numIntVars, applied.numIntVars, "${p.id} returned a malformed problem")
         }
     }
 
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ProbingTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ProbingTest.kt
index 1d5db7665..36f988ef0 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ProbingTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/ProbingTest.kt
@@ -3,20 +3,21 @@ package com.eignex.klause.presolve
 import com.eignex.klause.factor.arithmetic.LinearOp
 import com.eignex.klause.factor.arithmetic.ReifiedLinear
 import com.eignex.klause.factor.bool.Clause
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
+import com.eignex.klause.solver.Cancellation
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Lit
 import com.eignex.klause.solver.Problem
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 /**
  * Probing to fixpoint ([Presolve.probe]). Asserts the pass's observable output — the unit [Clause]s
  * and domain tightenings it derives — for failed literals, both-polarity bound tightening, the no-op
- * identity return, and a one-sided-consequence soundness guard. The cap is large enough that every
+ * empty delta, and a one-sided-consequence soundness guard. The cap is large enough that every
  * fixture is fully probed.
  */
 class ProbingTest {
@@ -26,6 +27,9 @@ class ProbingTest {
     private fun units(problem: Problem): List<Int> =
         problem.factors.filterIsInstance<Clause>().filter { it.literals.size == 1 }.map { it.literals[0] }
 
+    private fun probed(problem: Problem): Problem =
+        problem.withPassDelta(Presolve.probe(problem, cap, Cancellation.Never), BakeConfig.NONE)
+
     /** Whether [ints] is feasible against [problem] (every int pinned, propagation not Unsat). */
     private fun isFeasible(problem: Problem, ints: IntArray, bools: BooleanArray): Boolean {
         var a = Assumptions.None
@@ -71,7 +75,7 @@ class ProbingTest {
                 Clause(intArrayOf(Lit.make(0, false), Lit.make(1, false))),
             ),
         )
-        val out = Presolve.probe(problem, cap)
+        val out = probed(problem)
         assertTrue(Lit.make(0, false) in units(out), "fixing b0 = true conflicts ⇒ b0 forced false")
         assertEquals(feasibleAssignments(problem), feasibleAssignments(out), "feasibility set changed")
     }
@@ -103,7 +107,7 @@ class ProbingTest {
                 Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true))),
             ),
         )
-        val out = Presolve.probe(problem, cap)
+        val out = probed(problem)
         assertEquals(2, out.intDomains[0].min, "the common lower bound x ≥ 2 is folded in")
         assertEquals(feasibleAssignments(problem), feasibleAssignments(out), "feasibility set changed")
     }
@@ -127,7 +131,7 @@ class ProbingTest {
                 ),
             ),
         )
-        val out = Presolve.probe(problem, cap)
+        val out = probed(problem)
         assertEquals(0, out.intDomains[0].min, "a one-sided bound must not be applied")
         assertTrue(units(out).isEmpty(), "no literal failed")
         assertEquals(feasibleAssignments(problem), feasibleAssignments(out), "feasibility set changed")
@@ -142,6 +146,9 @@ class ProbingTest {
             intDomains = emptyArray(),
             factors = listOf(Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true)))),
         )
-        assertSame(problem, Presolve.probe(problem, cap), "nothing derivable is the pass's no-op signal")
+        assertTrue(
+            Presolve.probe(problem, cap, Cancellation.Never).isEmpty,
+            "nothing derivable is the pass's no-op signal",
+        )
     }
 }
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/RedundantConstraintsTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/RedundantConstraintsTest.kt
index a1d2d685a..2dddcf000 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/RedundantConstraintsTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/RedundantConstraintsTest.kt
@@ -8,6 +8,7 @@ import com.eignex.klause.factor.bool.PseudoBoolean
 import com.eignex.klause.factor.global.AllDifferent
 import com.eignex.klause.factor.global.Increasing
 import com.eignex.klause.model.PbOp
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.IntDomain
@@ -15,7 +16,6 @@ import com.eignex.klause.solver.Lit
 import com.eignex.klause.solver.Problem
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 /**
@@ -50,12 +50,13 @@ class RedundantConstraintsTest {
     }
 
     private fun checkPreserved(name: String, problem: Problem, expectDrop: Boolean): Problem {
-        val out = Presolve.removeRedundantConstraints(problem)
+        val delta = Presolve.removeRedundantConstraints(problem)
+        val out = problem.withPassDelta(delta, BakeConfig.NONE)
         assertEquals(feasibleCount(problem), feasibleCount(out), "$name: feasible set changed")
         if (expectDrop) {
             assertTrue(out.factors.size < problem.factors.size, "$name: expected a constraint to be dropped")
         } else {
-            assertSame(problem, out, "$name: expected no change")
+            assertTrue(delta.isEmpty, "$name: expected no change")
         }
         return out
     }
@@ -243,12 +244,13 @@ class RedundantConstraintsTest {
     }
 
     private fun checkPbPreserved(name: String, problem: Problem, expectDrop: Boolean): Problem {
-        val out = Presolve.removeRedundantConstraints(problem)
+        val delta = Presolve.removeRedundantConstraints(problem)
+        val out = problem.withPassDelta(delta, BakeConfig.NONE)
         assertEquals(feasibleCountBools(problem), feasibleCountBools(out), "$name: feasible set changed")
         if (expectDrop) {
             assertTrue(out.factors.size < problem.factors.size, "$name: expected a constraint to be dropped")
         } else {
-            assertSame(problem, out, "$name: expected no change")
+            assertTrue(delta.isEmpty, "$name: expected no change")
         }
         return out
     }
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/RootBakerTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/RootBakerTest.kt
new file mode 100644
index 000000000..1d46e1b70
--- /dev/null
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/RootBakerTest.kt
@@ -0,0 +1,140 @@
+package com.eignex.klause.presolve
+
+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.factor.table.Table
+import com.eignex.klause.propagation.PropagationResult
+import com.eignex.klause.solver.Cancellation
+import com.eignex.klause.solver.Factor
+import com.eignex.klause.solver.IntDomain
+import com.eignex.klause.solver.Lit
+import com.eignex.klause.solver.Problem
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+
+class RootBakerTest {
+
+    private fun bake(problem: Problem, config: BakeConfig): PropagationResult = RootBaker.bake(problem, config)
+
+    @Test
+    fun `failed-literal probing pins a forced literal`() {
+        // (a ∨ b), (a ∨ c), (¬b ∨ ¬c). Base propagation forces nothing; probing a=false forces b and c,
+        // then (¬b ∨ ¬c) fails, so a must be true.
+        val p = Problem(
+            numBoolVars = 3,
+            numIntVars = 0,
+            intDomains = emptyArray(),
+            factors = arrayOf<Factor>(
+                Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true))),
+                Clause(intArrayOf(Lit.make(0, true), Lit.make(2, true))),
+                Clause(intArrayOf(Lit.make(1, false), Lit.make(2, false))),
+            ),
+        )
+        val baked = assertIs<PropagationResult.Implied>(bake(p, BakeConfig(probeFailedLiterals = true)))
+        assertEquals(true, baked.boolValueOrNull(0), "probing should have forced a=true")
+    }
+
+    @Test
+    fun `failed-literal probing detects Unsat when both polarities fail`() {
+        val p = Problem(
+            numBoolVars = 1,
+            numIntVars = 0,
+            intDomains = emptyArray(),
+            factors = arrayOf<Factor>(
+                Clause(intArrayOf(Lit.make(0, true))),
+                Clause(intArrayOf(Lit.make(0, false))),
+            ),
+        )
+        assertIs<PropagationResult.Unsat>(bake(p, BakeConfig(probeFailedLiterals = true)))
+    }
+
+    @Test
+    fun `bound SAC tightens an int min when its lowest value is locally infeasible`() {
+        // x = y, x + y ≥ 2 over [0..3]^2. Bound-SAC probing x=0 finds x+y=0 < 2 infeasible → x.min ≥ 1.
+        val p = Problem(
+            numBoolVars = 0,
+            numIntVars = 2,
+            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
+            factors = arrayOf<Factor>(
+                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
+                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.GE, bound = 2),
+            ),
+        )
+        val baked = assertIs<PropagationResult.Implied>(bake(p, BakeConfig(probeIntBounds = true)))
+        assertEquals(1, baked.intMinOrNullCompat(0), "bound SAC should have lifted x.min to 1")
+        assertEquals(1, baked.intMinOrNullCompat(1), "bound SAC should have lifted y.min to 1")
+    }
+
+    @Test
+    fun `interior-hole SAC excludes an unreachable middle value`() {
+        // Allowed tuples (0,0) and (3,3); interior values 1, 2 are excluded by interior-hole SAC.
+        val p = Problem(
+            numBoolVars = 0,
+            numIntVars = 2,
+            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
+            factors = arrayOf<Factor>(
+                Table(xs = intArrayOf(0, 1), tuples = intArrayOf(0, 0, 3, 3)),
+            ),
+        )
+        val baked = assertIs<PropagationResult.Implied>(
+            bake(p, BakeConfig(probeIntBounds = true, probeIntHoles = true)),
+        )
+        val xHoles = mutableSetOf<Int>()
+        baked.forEachIntHole { id, v -> if (id == 0) xHoles.add(v) }
+        assertEquals(setOf(1, 2), xHoles, "interior-hole SAC should mark x ≠ 1 and x ≠ 2")
+    }
+
+    @Test
+    fun `per-var budget caps the probe count`() {
+        // With a per-var budget of 1, only the first probe per var runs. The downstream Linear
+        // propagation may still lift y.min indirectly, so we only assert x's min came in tighter.
+        val p = Problem(
+            numBoolVars = 0,
+            numIntVars = 2,
+            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
+            factors = arrayOf<Factor>(
+                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
+                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.GE, bound = 2),
+            ),
+        )
+        val baked = assertIs<PropagationResult.Implied>(
+            bake(p, BakeConfig(probeIntBounds = true, probeBudgetPerVar = 1)),
+        )
+        assertEquals(1, baked.intMinOrNullCompat(0))
+    }
+
+    @Test
+    fun `cancellation mid-bake yields a sound partial bake`() {
+        // A cancellation that has already fired stops probing before it enters any phase, so the bake is
+        // just the base bake — sound (probing only ever tightens, so skipping it forgoes tightening only).
+        val cancelled = Cancellation { true }
+        val p = Problem(
+            numBoolVars = 0,
+            numIntVars = 2,
+            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
+            factors = arrayOf<Factor>(
+                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
+                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.GE, bound = 2),
+            ),
+            cancellation = cancelled,
+        )
+        val baked = assertIs<PropagationResult.Implied>(bake(p, BakeConfig(probeIntBounds = true)))
+        assertEquals(null, baked.intMinOrNullCompat(0), "a fired cancellation should skip SAC tightening")
+    }
+
+    @Test
+    fun `no tier enabled returns the base bake unchanged`() {
+        val p = Problem(
+            numBoolVars = 0,
+            numIntVars = 2,
+            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
+            factors = arrayOf<Factor>(
+                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
+                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.GE, bound = 2),
+            ),
+        )
+        assertEquals(p.baked, bake(p, BakeConfig.NONE))
+    }
+}
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/StructuralReductionTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/StructuralReductionTest.kt
index d0961d02d..1841e00ee 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/StructuralReductionTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/StructuralReductionTest.kt
@@ -7,12 +7,12 @@ import com.eignex.klause.factor.global.AllDifferent
 import com.eignex.klause.factor.scheduling.Cumulative
 import com.eignex.klause.factor.scheduling.Disjunctive
 import com.eignex.klause.factor.table.Element
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.solver.IntDomain
 import com.eignex.klause.solver.Lit
 import com.eignex.klause.solver.Problem
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 /**
@@ -33,7 +33,7 @@ class StructuralReductionTest {
             arrayOf(IntDomain(2, 2), IntDomain(0, 100)),
             listOf(Element(idx = 0, result = 1, arr = intArrayOf(10, 20, 30), arrIsVars = false)),
         )
-        val out = Presolve.reduceStructural(problem)
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
         assertTrue(out.factors.none { it is Element }, "the element global is removed")
         val eq = theLinear(out)
         assertEquals(LinearOp.EQ, eq.op)
@@ -50,7 +50,7 @@ class StructuralReductionTest {
             Array(5) { IntDomain(0, 9) }.also { it[0] = IntDomain(1, 1) },
             listOf(Element(idx = 0, result = 1, arr = intArrayOf(2, 3, 4), arrIsVars = true)),
         )
-        val out = Presolve.reduceStructural(problem)
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
         assertTrue(out.factors.none { it is Element }, "the element global is removed")
         val eq = theLinear(out)
         assertEquals(LinearOp.EQ, eq.op)
@@ -67,7 +67,7 @@ class StructuralReductionTest {
             Array(3) { IntDomain(0, 9) }.also { it[0] = IntDomain(1, 1) },
             listOf(Element(idx = 0, result = 1, arr = intArrayOf(1, 2), arrIsVars = true)),
         )
-        val out = Presolve.reduceStructural(problem)
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
         assertTrue(out.factors.isEmpty(), "the vacuous element drops with no replacement")
     }
 
@@ -80,7 +80,7 @@ class StructuralReductionTest {
             arrayOf(IntDomain(0, 5), IntDomain(0, 10)),
             listOf(Element(idx = 0, result = 1, arr = intArrayOf(7, 7, 7), arrIsVars = false)),
         )
-        val out = Presolve.reduceStructural(problem)
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
         assertTrue(out.factors.none { it is Element }, "the element global is removed")
         assertEquals(7, theLinear(out).bound)
         assertEquals(1, out.intDomains[0].min, "index lower bound clamped to the array's first position")
@@ -95,7 +95,7 @@ class StructuralReductionTest {
             arrayOf(IntDomain(1, 3), IntDomain(0, 100)),
             listOf(Element(idx = 0, result = 1, arr = intArrayOf(10, 20, 30), arrIsVars = false)),
         )
-        assertSame(problem, Presolve.reduceStructural(problem), "no fixed index and a varied array is the no-op signal")
+        assertTrue(Presolve.reduceStructural(problem).isEmpty, "no fixed index and a varied array is the no-op signal")
     }
 
     @Test
@@ -106,7 +106,7 @@ class StructuralReductionTest {
             arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
             listOf(AllDifferent(intArrayOf(0, 1), domainMin = 0, domainSize = 4)),
         )
-        val out = Presolve.reduceStructural(problem)
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
         assertTrue(out.factors.none { it is AllDifferent }, "the all-different global is removed")
         val ne = theLinear(out)
         assertEquals(LinearOp.NE, ne.op)
@@ -122,7 +122,7 @@ class StructuralReductionTest {
             arrayOf(IntDomain(0, 3), IntDomain(0, 3), IntDomain(0, 3)),
             listOf(AllDifferent(intArrayOf(0, 1, 2), domainMin = 0, domainSize = 4)),
         )
-        assertSame(problem, Presolve.reduceStructural(problem), "a 3-var all-different keeps its global form")
+        assertTrue(Presolve.reduceStructural(problem).isEmpty, "a 3-var all-different keeps its global form")
     }
 
     @Test
@@ -134,7 +134,8 @@ class StructuralReductionTest {
             emptyArray(),
             listOf(Cardinality(intArrayOf(Lit.make(0, true), Lit.make(1, true), Lit.make(2, true)), min = 0, max = 3)),
         )
-        assertTrue(Presolve.reduceStructural(problem).factors.isEmpty(), "the vacuous cardinality drops")
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
+        assertTrue(out.factors.isEmpty(), "the vacuous cardinality drops")
     }
 
     @Test
@@ -145,7 +146,7 @@ class StructuralReductionTest {
             emptyArray(),
             listOf(Cardinality(intArrayOf(Lit.make(0, true), Lit.make(1, true), Lit.make(2, true)), min = 0, max = 1)),
         )
-        assertSame(problem, Presolve.reduceStructural(problem), "an at-most-one still constrains, so it stays")
+        assertTrue(Presolve.reduceStructural(problem).isEmpty, "an at-most-one still constrains, so it stays")
     }
 
     @Test
@@ -164,7 +165,7 @@ class StructuralReductionTest {
             ),
             listOf(AllDifferent(intArrayOf(0, 1, 2, 3, 4, 5), domainMin = 0, domainSize = 16)),
         )
-        val out = Presolve.reduceStructural(problem)
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
         val groups = out.factors.filterIsInstance<AllDifferent>().map { it.vars.toSet() }
         assertEquals(setOf(setOf(0, 1, 2), setOf(3, 4, 5)), groups.toSet(), "splits into the two value-disjoint groups")
     }
@@ -177,7 +178,7 @@ class StructuralReductionTest {
             arrayOf(IntDomain(0, 5), IntDomain(0, 5), IntDomain(0, 5)),
             listOf(AllDifferent(intArrayOf(0, 1, 2), domainMin = 0, domainSize = 6)),
         )
-        assertSame(problem, Presolve.reduceStructural(problem), "one connected component does not split")
+        assertTrue(Presolve.reduceStructural(problem).isEmpty, "one connected component does not split")
     }
 
     @Test
@@ -196,7 +197,7 @@ class StructuralReductionTest {
                 ),
             ),
         )
-        val out = Presolve.reduceStructural(problem)
+        val out = problem.withPassDelta(Presolve.reduceStructural(problem), BakeConfig.NONE)
         assertTrue(out.factors.none { it is Cumulative }, "the cumulative is removed")
         val disj = out.factors.filterIsInstance<Disjunctive>().single()
         assertEquals(listOf(0, 1, 2), disj.starts.toList())
@@ -217,6 +218,6 @@ class StructuralReductionTest {
                 ),
             ),
         )
-        assertSame(problem, Presolve.reduceStructural(problem), "tasks fit together, so it stays cumulative")
+        assertTrue(Presolve.reduceStructural(problem).isEmpty, "tasks fit together, so it stays cumulative")
     }
 }
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/SymmetryBreakingTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/SymmetryBreakingTest.kt
index 28477e1c6..e1c83cb48 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/SymmetryBreakingTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/SymmetryBreakingTest.kt
@@ -26,6 +26,7 @@ import com.eignex.klause.factor.table.Regular
 import com.eignex.klause.factor.table.Table
 import com.eignex.klause.localsearch.NoInvariant
 import com.eignex.klause.model.PbOp
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.Assumptions
 import com.eignex.klause.solver.Factor
@@ -77,8 +78,14 @@ class SymmetryBreakingTest {
         return count
     }
 
+    private fun broken(problem: Problem): Problem =
+        problem.withPassDelta(Presolve.breakSymmetries(problem), BakeConfig.NONE)
+
+    private fun precedence(problem: Problem): Problem =
+        problem.withPassDelta(Presolve.breakValuePrecedence(problem), BakeConfig.NONE)
+
     private fun checkSound(name: String, problem: Problem, expectReduced: Boolean) {
-        val broken = Presolve.breakSymmetries(problem)
+        val broken = broken(problem)
         val orig = countFeasible(problem)
         val after = countFeasible(broken)
         assertTrue(after <= orig, "$name: breaking ADDED solutions ($orig -> $after)")
@@ -86,7 +93,7 @@ class SymmetryBreakingTest {
         if (expectReduced) {
             assertTrue(after < orig, "$name: expected fewer solutions but $orig -> $after")
         } else {
-            assertSame(problem, broken, "$name: expected no symmetry detected")
+            assertTrue(Presolve.breakSymmetries(problem).isEmpty, "$name: expected no symmetry detected")
         }
     }
 
@@ -116,7 +123,7 @@ class SymmetryBreakingTest {
             Clause(intArrayOf(Lit.make(a, false), Lit.make(b, false))),
         )
         val problem = Problem(4, 0, emptyArray(), eq(0, 3) + eq(1, 2) + neq(0, 1) + neq(2, 3))
-        val broken = Presolve.breakSymmetries(problem)
+        val broken = broken(problem)
         assertEquals(
             countFeasible(problem) > 0,
             countFeasible(broken) > 0,
@@ -162,7 +169,7 @@ class SymmetryBreakingTest {
         // are the Bell(3)=5 set partitions, and the value_precede_chain keeps exactly one canonical
         // (restricted-growth) representative each — far stronger than pinning a single variable.
         val problem = Problem(0, 3, Array(3) { IntDomain(0, 2) }, emptyList())
-        val broken = Presolve.breakValuePrecedence(problem)
+        val broken = precedence(problem)
         val orig = countFeasible(problem)
         val after = countFeasible(broken)
         assertTrue(after < orig, "expected reduction: $orig -> $after")
@@ -180,7 +187,7 @@ class SymmetryBreakingTest {
             Array(3) { IntDomain(0, 2) },
             listOf(AllDifferent(intArrayOf(0, 1, 2), domainMin = 0, domainSize = 3)),
         )
-        val broken = Presolve.breakValuePrecedence(problem)
+        val broken = precedence(problem)
         assertEquals(6, countFeasible(problem))
         assertEquals(1, countFeasible(broken), "precedence + alldifferent should leave one solution")
     }
@@ -194,7 +201,7 @@ class SymmetryBreakingTest {
             Array(2) { IntDomain(0, 2) },
             listOf(Linear(intArrayOf(1, 2), intArrayOf(0, 1), LinearOp.LE, 3)),
         )
-        assertSame(problem, Presolve.breakValuePrecedence(problem), "no value symmetry ⇒ no-op")
+        assertTrue(Presolve.breakValuePrecedence(problem).isEmpty, "no value symmetry ⇒ no-op")
     }
 
     @Test
@@ -212,7 +219,7 @@ class SymmetryBreakingTest {
         assertEquals(6, countFeasible(problem))
         assertEquals(
             1,
-            countFeasible(Presolve.breakValuePrecedence(problem)),
+            countFeasible(precedence(problem)),
             "coloring value symmetry should collapse to one labeling",
         )
     }
@@ -243,7 +250,7 @@ class SymmetryBreakingTest {
             Array(2) { IntDomain(0, 2) },
             listOf(Linear(intArrayOf(1, -1), intArrayOf(0, 1), LinearOp.LE, 0)),
         )
-        assertSame(problem, Presolve.breakValuePrecedence(problem), "ordering ⇒ no value symmetry")
+        assertTrue(Presolve.breakValuePrecedence(problem).isEmpty, "ordering ⇒ no value symmetry")
     }
 
     @Test
@@ -264,7 +271,7 @@ class SymmetryBreakingTest {
                 ),
             ),
         )
-        val broken = Presolve.breakValuePrecedence(problem)
+        val broken = precedence(problem)
         val orig = countFeasible(problem)
         val after = countFeasible(broken)
         assertTrue(after < orig, "expected reduction: $orig -> $after")
@@ -342,7 +349,7 @@ class SymmetryBreakingTest {
         )
         checkSound("alldiff", problem, expectReduced = true)
         // 3! permutations collapse to the single sorted one.
-        assertEquals(1, countFeasible(Presolve.breakSymmetries(problem)))
+        assertEquals(1, countFeasible(broken(problem)))
     }
 
     @Test
@@ -426,7 +433,7 @@ class SymmetryBreakingTest {
                 PseudoBoolean(intArrayOf(1, 2, 4), intArrayOf(pos(3), pos(4), pos(5)), PbOp.LE, 5),
             ),
         )
-        val broken = Presolve.breakSymmetries(problem)
+        val broken = broken(problem)
         assertEquals(problem.numIntVars, broken.numIntVars, "dynamic handling must not grow the integer space")
         val symmetry = broken.factors.filterIsInstance<SymmetryHandling>().single()
         assertSame(NoInvariant, symmetry.asInvariant(), "symmetry handling must be propagator-only")
@@ -613,7 +620,7 @@ class SymmetryBreakingTest {
      *  it must never add solutions or flip satisfiability. Guards that a new structuralKey can't make
      *  verified detection unsound (a too-coarse key would). */
     private fun checkBreakingSound(name: String, problem: Problem) {
-        val broken = Presolve.breakSymmetries(problem)
+        val broken = broken(problem)
         val orig = countFeasible(problem)
         val after = countFeasible(broken)
         assertTrue(after <= orig, "$name: breaking ADDED solutions ($orig -> $after)")
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/XorUnitsTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/XorUnitsTest.kt
index 732d5bd56..51c8d89e8 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/presolve/XorUnitsTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/presolve/XorUnitsTest.kt
@@ -2,23 +2,26 @@ package com.eignex.klause.presolve
 
 import com.eignex.klause.factor.bool.Clause
 import com.eignex.klause.factor.bool.Xor
+import com.eignex.klause.presolve.PresolveShared.withPassDelta
 import com.eignex.klause.solver.Lit
 import com.eignex.klause.solver.Problem
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertSame
 import kotlin.test.assertTrue
 
 /**
  * GF(2) elimination over the root xor system ([Presolve.deriveXorUnits]). Asserts the pass's
  * observable output — the unit [Clause]s it appends — for forced literals, contradictions, derived
- * cross-row units, idempotence, and the no-op identity return.
+ * cross-row units, idempotence, and the no-op empty delta.
  */
 class XorUnitsTest {
 
     private fun units(problem: Problem): List<Int> =
         problem.factors.filterIsInstance<Clause>().filter { it.literals.size == 1 }.map { it.literals[0] }
 
+    private fun derived(problem: Problem): Problem =
+        problem.withPassDelta(Presolve.deriveXorUnits(problem), BakeConfig.NONE)
+
     @Test
     fun `a single-literal xor forces its variable with the right polarity`() {
         // targetParity xor negParity decides the value: a negated literal flips the forced polarity.
@@ -30,7 +33,7 @@ class XorUnitsTest {
         )
         for ((lit, parity, expected) in cases) {
             val problem = Problem(1, 0, emptyArray(), listOf(Xor(intArrayOf(lit), targetParity = parity)))
-            val out = Presolve.deriveXorUnits(problem)
+            val out = derived(problem)
             assertEquals(listOf(expected), units(out), "xor($lit)=$parity should force $expected")
         }
     }
@@ -47,7 +50,7 @@ class XorUnitsTest {
                 Xor(intArrayOf(Lit.make(1, true)), targetParity = 1),
             ),
         )
-        val out = Presolve.deriveXorUnits(problem)
+        val out = derived(problem)
         assertEquals(
             listOf(Lit.make(0, false), Lit.make(1, true), Lit.make(2, true)),
             units(out),
@@ -67,7 +70,7 @@ class XorUnitsTest {
                 Xor(intArrayOf(Lit.make(0, true), Lit.make(1, true), Lit.make(2, true)), targetParity = 1),
             ),
         )
-        val out = Presolve.deriveXorUnits(problem)
+        val out = derived(problem)
         assertEquals(listOf(Lit.make(2, true)), units(out), "the cross-row residue forces x2 = true")
     }
 
@@ -83,7 +86,7 @@ class XorUnitsTest {
                 Xor(intArrayOf(Lit.make(0, true)), targetParity = 0),
             ),
         )
-        val out = Presolve.deriveXorUnits(problem)
+        val out = derived(problem)
         assertEquals(
             setOf(Lit.make(0, true), Lit.make(0, false)),
             units(out).toSet(),
@@ -102,26 +105,24 @@ class XorUnitsTest {
                 Xor(intArrayOf(Lit.make(1, true)), targetParity = 1),
             ),
         )
-        val once = Presolve.deriveXorUnits(problem)
+        val once = derived(problem)
         assertEquals(
             setOf(Lit.make(0, true), Lit.make(1, true)),
             units(once).toSet(),
             "first run forces both variables",
         )
-        assertSame(once, Presolve.deriveXorUnits(once), "re-running adds no duplicate units")
+        assertTrue(Presolve.deriveXorUnits(once).isEmpty, "re-running adds no duplicate units")
     }
 
     @Test
-    fun `a problem with no xor factors is returned unchanged`() {
+    fun `a problem with no xor factors is a no-op`() {
         val problem = Problem(
             numBoolVars = 2,
             numIntVars = 0,
             intDomains = emptyArray(),
             factors = listOf(Clause(intArrayOf(Lit.make(0, true), Lit.make(1, false)))),
         )
-        val out = Presolve.deriveXorUnits(problem)
-        assertSame(problem, out, "no xor factors is the pass's no-op signal")
-        assertEquals(problem.factors, out.factors, "factor set is untouched")
-        assertTrue(out.factors.none { it is Xor }, "still no xor factors")
+        assertTrue(Presolve.deriveXorUnits(problem).isEmpty, "no xor factors is the pass's no-op signal")
+        assertTrue(problem.factors.none { it is Xor }, "still no xor factors")
     }
 }
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/propagation/PropagationStateMidlifeTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/propagation/PropagationStateMidlifeTest.kt
new file mode 100644
index 000000000..e04762000
--- /dev/null
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/propagation/PropagationStateMidlifeTest.kt
@@ -0,0 +1,98 @@
+package com.eignex.klause.propagation
+
+import com.eignex.klause.factor.arithmetic.Linear
+import com.eignex.klause.factor.arithmetic.LinearOp
+import com.eignex.klause.solver.Assumptions
+import com.eignex.klause.solver.Factor
+import com.eignex.klause.solver.IntDomain
+import com.eignex.klause.solver.Problem
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertNull
+
+/**
+ * The incremental-presolve mid-life factor API on [PropagationState]: appending a factor and
+ * tombstoning another between propagation rounds must reach the same root fixpoint as building the
+ * final factor set from scratch. Sound because the propagators are monotone, so the greatest
+ * fixpoint is unique regardless of the order factors are introduced or the ids they carry.
+ */
+class PropagationStateMidlifeTest {
+
+    // Three int vars, each 0..10. A fresh array per call — Problem construction folds root deductions
+    // into the domains it is given, so sharing one array across builds would cross-contaminate.
+    private fun domains() = arrayOf(IntDomain(0, 10), IntDomain(0, 10), IntDomain(0, 10))
+
+    private fun leq(coeffs: IntArray, vars: IntArray, bound: Int) = Linear(coeffs, vars, LinearOp.LE, bound)
+
+    private fun intBounds(state: PropagationState) =
+        (0 until state.problem.numIntVars).map { state.intDomains[it].min to state.intDomains[it].max }
+
+    /** Bake [factors] from scratch (non-incremental) and read the resulting int bounds. */
+    private fun freshBounds(factors: List<Factor>): List<Pair<Int, Int>> {
+        val state = PropagationState(Problem(0, 3, domains(), factors), Assumptions.None)
+        assertNull(state.runToFixpoint(allFactors = true))
+        return intBounds(state)
+    }
+
+    @Test
+    fun `an added mid-life factor propagates like a fresh build`() {
+        val base = leq(intArrayOf(1), intArrayOf(0), 5) // x0 <= 5
+        val added = leq(intArrayOf(1, -1), intArrayOf(1, 0), 0) // x1 <= x0
+
+        val state = PropagationState(Problem(0, 3, domains(), listOf(base)), Assumptions.None, incremental = true)
+        assertNull(state.runToFixpoint(allFactors = true))
+        state.addMidlifeFactor(added)
+        assertNull(state.runToFixpoint(allFactors = true))
+
+        assertEquals(freshBounds(listOf(base, added)), intBounds(state))
+        assertEquals(5, state.intDomains[1].max) // x1 tightened through x0
+    }
+
+    @Test
+    fun `a chain of mid-life factors propagates transitively like a fresh build`() {
+        val base = leq(intArrayOf(1), intArrayOf(0), 5) // x0 <= 5
+        val g = leq(intArrayOf(1, -1), intArrayOf(1, 0), 0) // x1 <= x0
+        val h = leq(intArrayOf(1, -1), intArrayOf(2, 1), 0) // x2 <= x1
+
+        val state = PropagationState(Problem(0, 3, domains(), listOf(base)), Assumptions.None, incremental = true)
+        assertNull(state.runToFixpoint(allFactors = true))
+        state.addMidlifeFactor(g)
+        state.addMidlifeFactor(h)
+        assertNull(state.runToFixpoint(allFactors = true))
+
+        assertEquals(freshBounds(listOf(base, g, h)), intBounds(state))
+        assertEquals(5, state.intDomains[2].max) // x2 tightened through the whole chain
+    }
+
+    @Test
+    fun `a tombstoned mid-life factor does not propagate`() {
+        val added = leq(intArrayOf(1), intArrayOf(0), 5) // x0 <= 5, never allowed to fire
+
+        val state = PropagationState(Problem(0, 3, domains(), emptyList()), Assumptions.None, incremental = true)
+        assertNull(state.runToFixpoint(allFactors = true))
+        val fid = state.addMidlifeFactor(added)
+        state.tombstoneFactor(fid)
+        assertNull(state.runToFixpoint(allFactors = true))
+
+        assertEquals(freshBounds(emptyList()), intBounds(state))
+        assertEquals(10, state.intDomains[0].max) // untouched — the tombstoned factor stayed inert
+    }
+
+    @Test
+    fun `tombstoning a redundant base factor matches a fresh build without it`() {
+        val kept = leq(intArrayOf(1), intArrayOf(0), 5) // x0 <= 5
+        val redundant = leq(intArrayOf(1), intArrayOf(0), 7) // x0 <= 7, implied by kept
+
+        val state = PropagationState(
+            Problem(0, 3, domains(), listOf(kept, redundant)),
+            Assumptions.None,
+            incremental = true,
+        )
+        assertNull(state.runToFixpoint(allFactors = true))
+        state.tombstoneFactor(1) // drop the redundant one by id
+        assertNull(state.runToFixpoint(allFactors = true))
+
+        assertEquals(freshBounds(listOf(kept)), intBounds(state))
+        assertEquals(5, state.intDomains[0].max)
+    }
+}
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/BoundSacProbingTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/BoundSacProbingTest.kt
deleted file mode 100644
index 7238cba97..000000000
--- a/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/BoundSacProbingTest.kt
+++ /dev/null
@@ -1,131 +0,0 @@
-package com.eignex.klause.solver.integration
-
-import com.eignex.klause.factor.arithmetic.Linear
-import com.eignex.klause.factor.arithmetic.LinearOp
-import com.eignex.klause.factor.table.Table
-import com.eignex.klause.propagation.PropagationResult
-import com.eignex.klause.solver.*
-import kotlin.test.Test
-import kotlin.test.assertEquals
-import kotlin.test.assertIs
-
-class BoundSacProbingTest {
-
-    @Test
-    fun `simplest SAC probe`() {
-        // Single var x ∈ [0..3], constraint x ≥ 2. Trivially propagates without SAC,
-        // but exercises the bake-time SAC path with only one var.
-        val p = Problem(
-            numBoolVars = 0,
-            numIntVars = 1,
-            intDomains = arrayOf(IntDomain(0, 3)),
-            factors = arrayOf<Factor>(
-                Linear(coeffs = intArrayOf(1), vars = intArrayOf(0), op = LinearOp.GE, bound = 2),
-            ),
-            probeIntBounds = true,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        // Either via direct propagation (x.min lifts to 2) or via SAC. Either way:
-        assertEquals(2, baked.intMinOrNullCompat(0) ?: 2)
-    }
-
-    @Test
-    fun `bound SAC tightens an int min when its lowest value is locally infeasible`() {
-        // x = y, x + y ≥ 2 over [0..3]^2. Pure linear bound prop alone can't combine
-        // the two; bound-SAC probing x=0 finds x+y=0 < 2 infeasible → x.min ≥ 1.
-        val p = Problem(
-            numBoolVars = 0,
-            numIntVars = 2,
-            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
-            factors = arrayOf<Factor>(
-                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
-                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.GE, bound = 2),
-            ),
-            probeIntBounds = true,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        assertEquals(1, baked.intMinOrNullCompat(0), "bound SAC should have lifted x.min to 1")
-        assertEquals(1, baked.intMinOrNullCompat(1), "bound SAC should have lifted y.min to 1")
-    }
-
-    @Test
-    fun `bound SAC narrows to singleton when only one value remains feasible`() {
-        val p = Problem(
-            numBoolVars = 0,
-            numIntVars = 2,
-            intDomains = arrayOf(IntDomain(0, 2), IntDomain(0, 2)),
-            factors = arrayOf<Factor>(
-                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
-                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 2),
-            ),
-            probeIntBounds = true,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        assertEquals(1, baked.intValueOrNull(0))
-        assertEquals(1, baked.intValueOrNull(1))
-    }
-
-    @Test
-    fun `interior-hole SAC excludes an unreachable middle value`() {
-        // Allowed tuples (0,0) and (3,3); interior values 1, 2 should be excluded by
-        // interior-hole SAC.
-        val p = Problem(
-            numBoolVars = 0,
-            numIntVars = 2,
-            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
-            factors = arrayOf<Factor>(
-                Table(
-                    xs = intArrayOf(0, 1),
-                    tuples = intArrayOf(0, 0, 3, 3),
-                ),
-            ),
-            probeIntBounds = true,
-            probeIntHoles = true,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        val xHoles = mutableSetOf<Int>()
-        baked.forEachIntHole { id, v -> if (id == 0) xHoles.add(v) }
-        assertEquals(setOf(1, 2), xHoles, "interior-hole SAC should mark x ≠ 1 and x ≠ 2")
-    }
-
-    @Test
-    fun `SAC budget caps probe count`() {
-        // Same setup as the lift-min test, but with a per-var budget of 1. Only enough
-        // calls for the v=0 min probe to land — the loop should exit before lifting y.
-        val p = Problem(
-            numBoolVars = 0,
-            numIntVars = 2,
-            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
-            factors = arrayOf<Factor>(
-                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
-                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.GE, bound = 2),
-            ),
-            probeIntBounds = true,
-            probeBudgetPerVar = 1,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        // With per-var budget 1, at most the first probe per var runs. The downstream
-        // Linear propagation from the first tightening may still lift y.min indirectly
-        // (the propagator chain isn't budget-limited), so we only assert the bound
-        // came in tighter than 0 for x — the loop completed without exceeding the cap.
-        assertEquals(1, baked.intMinOrNullCompat(0))
-    }
-
-    @Test
-    fun `bound SAC off does not tighten`() {
-        val p = Problem(
-            numBoolVars = 0,
-            numIntVars = 2,
-            intDomains = arrayOf(IntDomain(0, 3), IntDomain(0, 3)),
-            factors = arrayOf<Factor>(
-                Linear(coeffs = intArrayOf(1, -1), vars = intArrayOf(0, 1), op = LinearOp.EQ, bound = 0),
-                Linear(coeffs = intArrayOf(1, 1), vars = intArrayOf(0, 1), op = LinearOp.GE, bound = 2),
-            ),
-            probeIntBounds = false,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        // Without probing, bound stays at 0 (factor-local propagation can't combine the
-        // two constraints to lift the min).
-        assertEquals(null, baked.intMinOrNullCompat(0))
-    }
-}
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/FailedLiteralProbingTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/FailedLiteralProbingTest.kt
deleted file mode 100644
index 94aee8938..000000000
--- a/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/FailedLiteralProbingTest.kt
+++ /dev/null
@@ -1,107 +0,0 @@
-package com.eignex.klause.solver.integration
-
-import com.eignex.klause.factor.bool.Cardinality
-import com.eignex.klause.factor.bool.Clause
-import com.eignex.klause.propagation.PropagationResult
-import com.eignex.klause.solver.*
-import kotlin.test.Test
-import kotlin.test.assertEquals
-import kotlin.test.assertIs
-import kotlin.test.assertNull
-
-class FailedLiteralProbingTest {
-
-    @Test
-    fun `probing forces a literal when one polarity propagates Unsat`() {
-        // (a ∨ b), (a ∨ c), (¬b ∨ ¬c). Direct propagation forces nothing. Probing
-        // a=false forces b=true and c=true, then (¬b ∨ ¬c) fails → a must be true.
-        val p = Problem(
-            numBoolVars = 3,
-            numIntVars = 0,
-            intDomains = emptyArray(),
-            factors = arrayOf<Factor>(
-                Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true))),
-                Clause(intArrayOf(Lit.make(0, true), Lit.make(2, true))),
-                Clause(intArrayOf(Lit.make(1, false), Lit.make(2, false))),
-            ),
-            probeFailedLiterals = true,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        assertEquals(true, baked.bools[0], "probing should have forced a=true")
-    }
-
-    @Test
-    fun `probing off does not detect the failed literal`() {
-        val p = Problem(
-            numBoolVars = 3,
-            numIntVars = 0,
-            intDomains = emptyArray(),
-            factors = arrayOf<Factor>(
-                Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true))),
-                Clause(intArrayOf(Lit.make(0, true), Lit.make(2, true))),
-                Clause(intArrayOf(Lit.make(1, false), Lit.make(2, false))),
-            ),
-            probeFailedLiterals = false,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        assertNull(baked.bools[0], "without probing, var 0 stays free")
-    }
-
-    @Test
-    fun `probing detects Unsat when both polarities fail`() {
-        val p = Problem(
-            numBoolVars = 1,
-            numIntVars = 0,
-            intDomains = emptyArray(),
-            factors = arrayOf<Factor>(
-                Clause(intArrayOf(Lit.make(0, true))),
-                Clause(intArrayOf(Lit.make(0, false))),
-            ),
-            probeFailedLiterals = true,
-        )
-        assertIs<PropagationResult.Unsat>(p.baked)
-    }
-
-    @Test
-    fun `probing reaches fixpoint over multiple passes`() {
-        // Pass 1 forces a=true (via the (a∨b), (a∨c), (¬b∨¬c) triangle); pass 2 then
-        // chains through (¬a ∨ d) to force d=true.
-        val p = Problem(
-            numBoolVars = 4,
-            numIntVars = 0,
-            intDomains = emptyArray(),
-            factors = arrayOf<Factor>(
-                Clause(intArrayOf(Lit.make(0, true), Lit.make(1, true))),
-                Clause(intArrayOf(Lit.make(0, true), Lit.make(2, true))),
-                Clause(intArrayOf(Lit.make(1, false), Lit.make(2, false))),
-                Clause(intArrayOf(Lit.make(0, false), Lit.make(3, true))),
-            ),
-            probeFailedLiterals = true,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        assertEquals(true, baked.bools[0])
-        assertEquals(true, baked.bools[3])
-    }
-
-    @Test
-    fun `probing on a feasible problem with no forced literals leaves baked unchanged`() {
-        val p = Problem(
-            numBoolVars = 4,
-            numIntVars = 0,
-            intDomains = emptyArray(),
-            factors = arrayOf<Factor>(
-                Cardinality.exactlyOne(
-                    intArrayOf(
-                        Lit.make(0, true),
-                        Lit.make(1, true),
-                        Lit.make(2, true),
-                        Lit.make(3, true),
-                    ),
-                ),
-            ),
-            probeFailedLiterals = true,
-        )
-        val baked = assertIs<PropagationResult.Implied>(p.baked)
-        for (v in 0..3) assertNull(baked.bools[v], "var $v unexpectedly forced: $baked")
-    }
-}
diff --git a/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/ProblemDomainTighteningTest.kt b/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/ProblemDomainTighteningTest.kt
index 752a28912..be0891534 100644
--- a/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/ProblemDomainTighteningTest.kt
+++ b/klause/src/commonTest/kotlin/com/eignex/klause/solver/integration/ProblemDomainTighteningTest.kt
@@ -2,6 +2,8 @@ package com.eignex.klause.solver.integration
 
 import com.eignex.klause.factor.arithmetic.Linear
 import com.eignex.klause.factor.arithmetic.LinearOp
+import com.eignex.klause.presolve.BakeConfig
+import com.eignex.klause.presolve.RootBaker
 import com.eignex.klause.propagation.PropagationResult
 import com.eignex.klause.solver.*
 import kotlin.test.Test
@@ -64,14 +66,14 @@ class ProblemDomainTighteningTest {
 
     @Test
     fun `interior holes from SAC probing are excluded from the domain`() {
-        val p =
+        val base =
             Problem(
                 0,
                 1,
                 arrayOf(IntDomain(0, 4)),
                 listOf(Linear(intArrayOf(1), intArrayOf(0), LinearOp.NE, 2)),
-                probeIntHoles = true,
             )
+        val p = RootBaker.reseed(base, BakeConfig(probeIntHoles = true))
         assertIs<PropagationResult.Implied>(p.baked)
         assertFalse(2 in p.intDomains[0])
         assertTrue(1 in p.intDomains[0])