|
| 1 | +# Three serious algorithmic directions for `manthan.cpp` |
| 2 | + |
| 3 | +## Diagnosis (from `build/data/out-synth-1570930-0`) |
| 4 | + |
| 5 | +The death spiral on every long-tail benchmark looks the same: |
| 6 | + |
| 7 | +``` |
| 8 | +genbuf12b4y var 96 16264 repairs 121K AIG nodes depth 10860 |
| 9 | +ActivityService var 100 16300 repairs 258K AIG nodes depth 15374 |
| 10 | +sdlx-fixpoint-7 var 1023 176 repairs ~250 AIG nodes depth 19 |
| 11 | +``` |
| 12 | + |
| 13 | +Every `perform_repair` call does |
| 14 | +`compose_or(branch, old_formula)` |
| 15 | +where `branch = AND(literals of one SAT-solver conflict)`. After K repairs the |
| 16 | +per-variable AIG has depth ≈ K and node count ≈ K · |conflict|, and the |
| 17 | +formula's CNF mirror grows the same way. |
| 18 | + |
| 19 | +Three things follow: |
| 20 | + |
| 21 | +1. **Chain blowup is the bottleneck.** On ActivityService, `recompute_y_hat` |
| 22 | + (`AIG::evaluate` over the chained AIG, per y, per repair) is **33.5%** of |
| 23 | + total time, `cex_finding` 21.6%, `find_conflict` 11.3%. All three slow |
| 24 | + down quadratically as the chain grows. |
| 25 | +2. **Repairs barely generalize.** `avg rep/loop` collapses to **1.0** in the |
| 26 | + long tail — every CEX fixes a single corner of input space. |
| 27 | +3. **Cost-zero ratio is huge.** ActivityService: 57,781 cost-zero "repairs" |
| 28 | + out of 81,377 solver calls — wasted SAT calls where the wrong y-value was |
| 29 | + actually fine and only the downstream y's needed updating. |
| 30 | + |
| 31 | +The three fixes split along three orthogonal axes: |
| 32 | +**shrink what you build**, **learn more per repair**, or |
| 33 | +**rebuild instead of accumulating**. |
| 34 | + |
| 35 | +--- |
| 36 | + |
| 37 | +## Option 1 — Periodic per-variable AIG compaction + lazy CNF re-encoding |
| 38 | + |
| 39 | +### The idea |
| 40 | + |
| 41 | +Treat the chained AIG as the source of truth and never let it grow |
| 42 | +unboundedly. When a variable's per-formula AIG exceeds a threshold (e.g. |
| 43 | +depth > 100 or nodes > 2000), run `AIGRewriter::rewrite_all` + `sat_sweep` |
| 44 | ++ `rewrite_all` on it (the same passes already used in |
| 45 | +`bve_and_substitute`), then **discard** `var_to_formula[y].clauses` / |
| 46 | +`out` and re-Tseitin from the compacted AIG via `AIGToCNF`. Reset |
| 47 | +`uninserted_start = 0` so `inject_formulas_into_solver` sees the new |
| 48 | +clauses; keep the old indicator alive (or rebind via a fresh |
| 49 | +equivalence) so `cex_solver` doesn't get confused. |
| 50 | + |
| 51 | +### Why it should work |
| 52 | + |
| 53 | +Most repair conflicts overlap heavily — the chained ORs accumulate |
| 54 | +ITE-equivalent and constant-propagatable structure that the AIG rewriter |
| 55 | +already knows how to crush. The `bve_and_substitute` log shows >40% |
| 56 | +reduction routinely on initial AIGs; on a chain of 16k repairs the |
| 57 | +compression is likely 10–100× because each repair conflict is a |
| 58 | +near-duplicate of prior ones. |
| 59 | + |
| 60 | +### Plan (~300–500 LOC) |
| 61 | + |
| 62 | +- Add `aig_compact_threshold_depth`, `_nodes`, and |
| 63 | + `aig_compact_check_every` (e.g. every 100 repairs per var, or in the |
| 64 | + main repair loop after a CEX round) to `ManthanConf`. |
| 65 | +- `Manthan::compact_var_formula(uint32_t y)`: take |
| 66 | + `var_to_formula[y].aig`, run rewriter, re-encode via a fresh |
| 67 | + `AIGToCNF`, replace `var_to_formula[y]` and push to `updated_y_funcs`. |
| 68 | +- Sub-AIG dependencies: when y's AIG references other y_hats, the |
| 69 | + compaction is *local* — leaves are y_hat lits or input lits; that's |
| 70 | + already what `bve_and_substitute` does at line 979 |
| 71 | + (`AIG::translate_leaves`). |
| 72 | +- The compaction creates a new `f.out` (Tseitin var) — the old indicator |
| 73 | + (`y_hat_to_indic`) needs to be re-bound. Either drop the old indicator |
| 74 | + entry and call `add_not_f_x_yhat`-style fresh, or wrap with an |
| 75 | + equivalence clause `new_out ↔ old_out`. |
| 76 | + |
| 77 | +### Risk |
| 78 | + |
| 79 | +Indicator lifecycle is the only landmine — there's a `SLOW_DEBUG` check |
| 80 | +(`check_aig_matches_clauses_per_formula`) that will catch divergence |
| 81 | +loudly. Otherwise low: it's a representation transformation, not an |
| 82 | +algorithm change. |
| 83 | + |
| 84 | +### Expected impact |
| 85 | + |
| 86 | +Directly attacks the 33%+ `recompute_y_hat` cost and the |
| 87 | +linear-in-repairs growth. Probably wins ~10–20 of the timeout instances |
| 88 | +where Manthan was making real progress but drowning in formula bloat |
| 89 | +(sdlx-fixpoint-{4,5,6,7}, ActivityService, factorization). |
| 90 | + |
| 91 | +--- |
| 92 | + |
| 93 | +## Option 2 — Craig-interpolant repair clauses |
| 94 | + |
| 95 | +### The idea |
| 96 | + |
| 97 | +Replace "the SAT conflict" as the repair clause with a **Craig |
| 98 | +interpolant** computed over the input variables only. |
| 99 | + |
| 100 | +When `find_conflict` returns UNSAT, the proof is a refutation of |
| 101 | +`(F(x,y) ∧ y_others = ctx[y_others] ∧ y_rep = ¬ctx[y_rep])` plus |
| 102 | +assumptions on the inputs. Partition (A, B) for the McMillan |
| 103 | +interpolant: |
| 104 | + |
| 105 | +- A = `F(x,y) ∧ y_others = ctx[y_others] ∧ y_rep = ¬ctx[y_rep]` |
| 106 | +- B = `x = ctx[x]` (the input assumptions) |
| 107 | + |
| 108 | +Shared variables = input variables. The interpolant `I(x)` satisfies: |
| 109 | + |
| 110 | +- `A → I(x)` — captures the entire region of inputs for which flipping |
| 111 | + `y_rep` is feasible (i.e. where the current value is *required*). |
| 112 | +- `I(x) ∧ B` is UNSAT — the original CEX input is excluded. |
| 113 | + |
| 114 | +So the **repair function** to add is: |
| 115 | + |
| 116 | +``` |
| 117 | +if ctx[y_rep] = TRUE : y_rep_func ← y_rep_func OR (¬I(x)) |
| 118 | +if ctx[y_rep] = FALSE: y_rep_func ← y_rep_func AND I(x) |
| 119 | +``` |
| 120 | + |
| 121 | +Today we do `compose_or` with `AND(literals of one corner)`. Tomorrow we |
| 122 | +do `compose_or` with the interpolant AIG, which typically subsumes |
| 123 | +thousands of would-be conflict clauses. |
| 124 | + |
| 125 | +### Why it should work |
| 126 | + |
| 127 | +The "1 repair per loop, repeated 16k times" pattern is the textbook |
| 128 | +symptom of conflict-clause learning vs interpolant-based learning. |
| 129 | +IC3/PDR moved from clausal blocking to interpolant-style inductive |
| 130 | +frames for exactly this reason. Each repair would now generalize to a |
| 131 | +region rather than a singleton. |
| 132 | + |
| 133 | +### Plan (~1500 LOC, harder) |
| 134 | + |
| 135 | +There is already an `Interpolant` infrastructure in `src/interpolant.h` |
| 136 | +/ `interpolant.cpp` that we use in `backward.cpp` for the |
| 137 | +doubled-variable equivalence trick (Bonacina-Ghilardi). We can adapt |
| 138 | +it: it already uses CaDiCaL with a `Tracer` (`MyTracer`) that consumes |
| 139 | +proof antecedents on the fly and folds them into a McMillan |
| 140 | +interpolant AIG. |
| 141 | + |
| 142 | +- Pick interpolation backend: reuse the existing `MyTracer` / |
| 143 | + `Interpolant` (uses CaDiCaL's antecedent-tracking |
| 144 | + `connect_proof_tracer`). Lower risk than a from-scratch DRAT pass. |
| 145 | +- Build a **mirror cadical solver** whose state matches `repair_solver` |
| 146 | + (same input clauses, same cumulative learned formula clauses), with |
| 147 | + proof tracing on. When `find_conflict` returns UNSAT, replay the same |
| 148 | + assumptions on the mirror, fetch the interpolant AIG. |
| 149 | +- Pass the interpolant AIG into `perform_repair` as a precomputed |
| 150 | + branch; `compose_or/and` are unchanged. |
| 151 | +- SLOW_DEBUG: check that `I(ctx[x]) = FALSE` and that the new repaired |
| 152 | + formula is correct via `check_aig_matches_clauses_per_formula`. |
| 153 | +- Fallback: if the interpolation engine fails, the interpolant is huge, |
| 154 | + or the mirror can't be kept in sync, fall back to today's |
| 155 | + conflict-clause behavior. |
| 156 | + |
| 157 | +### Risk |
| 158 | + |
| 159 | +Interpolation engines need careful state management; bugs surface as |
| 160 | +wrong synthesis silently. SLOW_DEBUG + `check_repair_monotonic` catch |
| 161 | +most of these. Mirror-solver state synchronization is the biggest |
| 162 | +operational risk. |
| 163 | + |
| 164 | +### Expected impact |
| 165 | + |
| 166 | +Could be transformative — the chain-of-corners pattern collapses to |
| 167 | +chain-of-regions. On benchmarks where the function has a clean Boolean |
| 168 | +structure (most of factorization, genbuf, amba), a handful of |
| 169 | +interpolants may suffice where today thousands of conflicts are needed. |
| 170 | +But: on benchmarks where the function genuinely has no clean structure, |
| 171 | +interpolants degrade to clausal conflicts and we gain nothing. |
| 172 | + |
| 173 | +--- |
| 174 | + |
| 175 | +## Option 3 — Trigger-based per-variable function re-synthesis |
| 176 | + |
| 177 | +### The idea |
| 178 | + |
| 179 | +Stop *patching* a hot variable; *rebuild* it. When a y has been |
| 180 | +repaired more than N times (e.g. 200), the chained AIG is almost |
| 181 | +certainly a worse representation than what we could synthesize from |
| 182 | +scratch: |
| 183 | + |
| 184 | +- Take all the (input, correct y) pairs we've seen via CEX history |
| 185 | + (these are *adversarial* — far better than random samples). |
| 186 | +- Take y's input support from `aig_dep_list` (already cached in |
| 187 | + `dep_cache`). |
| 188 | +- Train a **decision tree** on this support (the existing `ManthanLearn` |
| 189 | + infrastructure), or do **SAT-based exact synthesis** with templates of |
| 190 | + growing size (k-LUT, AND/OR with ≤ N gates). |
| 191 | +- Verify the candidate with one cex_solver round; if it has fewer |
| 192 | + error CEXs than the chain, atomically replace `var_to_formula[y]` |
| 193 | + with the new AIG. If not, revert. |
| 194 | +- Reset the per-var repair counter and continue. |
| 195 | + |
| 196 | +### Why it should work |
| 197 | + |
| 198 | +The chains we're growing are pathological encodings of relatively small |
| 199 | +Boolean functions. A single decision tree of depth 20 over a |
| 200 | +30-variable support can encode what 10,000 conflict-OR layers encode; |
| 201 | +an exact-synth template of 50 gates can do the same. The existing |
| 202 | +`--manthan_base 0` (LEARN) path does this *upfront* on random samples. |
| 203 | +The novel piece is doing it **mid-loop, on demand, with adversarial |
| 204 | +samples**. |
| 205 | + |
| 206 | +### Plan (~600 LOC) |
| 207 | + |
| 208 | +- Add `mconf.resynth_after_repairs` (e.g. 200) and |
| 209 | + `mconf.resynth_min_support` (e.g. 4). |
| 210 | +- Persist a per-var `vector<sample> y_cex_history`; append every sample |
| 211 | + that put y in `needs_repair`. Cap at ~5k samples. |
| 212 | +- New `Manthan::resynth_var(uint32_t y)`: |
| 213 | + - extract support from `dep_cache[y].dep_list`, |
| 214 | + - call `ManthanLearn::train_one_var(y, support, samples)` (already |
| 215 | + exists in `manthan_learn.cpp` as the per-var path), |
| 216 | + - convert decision tree to AIG (already exists), |
| 217 | + - encode via `AIGToCNF`, |
| 218 | + - run a quick *narrow* cex check: `repair_solver.solve` with |
| 219 | + assumptions forcing the new y to differ from the old y's correct |
| 220 | + outputs; if no easy CEX, swap formulas in. |
| 221 | +- Keep the chain as a fallback if resynth's verifier fails. |
| 222 | + |
| 223 | +### Risk |
| 224 | + |
| 225 | +Two real ones: (1) replacing the formula breaks |
| 226 | +indicator/dependency invariants — same lifecycle care as Option 1; (2) |
| 227 | +we may *lose* progress (the resynthesized fn could be worse than the |
| 228 | +chain on regions we'd already learned). Mitigate by verifying narrowly |
| 229 | +and reverting on regression, plus boosting `prev_error_count` |
| 230 | +monotonicity check via `check_repair_monotonic`. |
| 231 | + |
| 232 | +### Expected impact |
| 233 | + |
| 234 | +Targeted at the worst offenders — the `var 96` / `var 100` cases that |
| 235 | +consume 90%+ of time on a single benchmark. If resynth succeeds on even |
| 236 | +one such var, the rest of that benchmark often falls in seconds. If it |
| 237 | +fails, you spend a few thousand SAT calls, give up, and continue. |
| 238 | + |
| 239 | +--- |
| 240 | + |
| 241 | +## Ranking |
| 242 | + |
| 243 | +- **Highest expected ROI per LOC: Option 1.** Chain growth is currently |
| 244 | + uncontrolled, and the AIG rewriter is right there. Probably 1–2 days; |
| 245 | + most work is testing the indicator lifecycle. |
| 246 | +- **Biggest possible algorithmic win: Option 2.** This is the "real" |
| 247 | + generalization story. 1–2 weeks; real risk of subtle bugs; if it |
| 248 | + lands, the long-tail benchmarks become easy. |
| 249 | +- **Complementary force-multiplier: Option 3.** Doesn't compete with 1 |
| 250 | + or 2 — could be added on top of either. Best as a follow-up once |
| 251 | + Option 1 has tamed the bloat enough that re-synthesis sees clean |
| 252 | + inputs. |
0 commit comments