Sum the crossing count scaled by the inside width in the T term

src/decompose/portfolio/tests/driver.rs

@@ -26,12 +26,15 @@ use std::sync::Arc;
 /// (flowcutter-incidence/flowcutter-primal/goatd/hypergraph-bisect/
 /// guided-bisect) — investigate, do not just relax it.
 ///
-/// The expected winner is `hypergraph-bisect:imbalance=0.40` on the generated
-/// multiplier fixture. It is a property of the fixture, not a target:
-/// regenerating the fixture at a different width means re-observing this,
-/// never editing it to match a one-off run. Peak-mode ranks by context width
-/// while the conversion searches on cost, so a decomposition candidate's peak
-/// width moves when the reading it settles on moves.
+/// The expected winner is `flowcutter-primal` on the generated multiplier
+/// fixture. It is a property of the fixture, not a target: regenerating the
+/// fixture at a different width means re-observing this, never editing it to
+/// match a one-off run. Peak-mode ranks by context width while the conversion
+/// searches on cost, so a decomposition candidate's peak width moves when the
+/// reading it settles on moves — it was `hypergraph-bisect:imbalance=0.40`
+/// while the cost summed the tight width, and was re-observed as
+/// `flowcutter-primal` in five of five runs once the cost summed the crossing
+/// count scaled by the inside width.
 #[test]
 fn peak_mode_selection_pin() {
     let formula = crate::tests::circuit_fixture::multiplier();
@@ -47,7 +50,7 @@ fn peak_mode_selection_pin() {
     .expect("portfolio");
     assert_eq!(
         built.selection.winning_spec.as_deref(),
-        Some("hypergraph-bisect:imbalance=0.40"),
+        Some("flowcutter-primal"),
         "peak-mode selection changed"
     );
     assert!(

src/score/mod.rs

@@ -127,14 +127,17 @@ pub(crate) fn vtree_clause_load_per_node(vtree: &Vtree, formula: &CnfFormula) ->
 /// Combined structural cost of a vtree: lower is better.
 ///
 /// Every internal node `t` splits the formula's variables into the ones below
-/// it and the rest. Let `w0(t)` and `w1(t)` be the smallest and second-smallest
-/// of its inside-context width, outside-context width, and crossing-clause
-/// count. The width terms are
+/// it and the rest. Let `in(t)` be its inside-context width, `cross(t)` its
+/// crossing-clause count, `m` the formula's clause count, and `w0(t)` and
+/// `w1(t)` the smallest and second-smallest of its inside-context width,
+/// outside-context width, and crossing-clause count. The width terms are
 ///
 /// ```text
-/// T = log₂ Σ_t 2^w0(t)
-/// E = max(0, log₂ Σ_t 2^(w0(t) + min(7, w1(t) - w0(t))) - T
-///            - log₂(1 + max(0, log₂ Σ_t 2^(cross(left(t)) + cross(right(t))) - T)))
+/// w(t) = cross(t) in(t) / m
+/// T  = log₂ Σ_t 2^w(t)
+/// T0 = log₂ Σ_t 2^w0(t)
+/// E  = max(0, log₂ Σ_t 2^(w0(t) + min(7, w1(t) - w0(t))) - T0
+///             - log₂(1 + max(0, log₂ Σ_t 2^(cross(left(t)) + cross(right(t))) - T0)))
 /// ```
 ///
 /// where leaf crossing counts are capped at one and every sum omits zero
@@ -214,15 +217,32 @@ fn log2_sum_exp(values: &[f64]) -> f64 {
         .log2()
 }
 
+/// The width of one internal cut for the `T` term: the crossing-clause count
+/// scaled by the inside width over the clause count. It is at most the inside
+/// width, and is the inside width when every clause crosses the cut.
+///
+/// It is not the smallest of the three bounds, which the excess term still
+/// measures against. As the width `T` sums, that minimum favours a cut whose
+/// outside width is small, and the chain a shallow edge-binarized reading
+/// builds keeps the outside width small at every node while carrying most of
+/// the formula across each cut. Those trees do not compile: on 44 formulas
+/// with six trees each, the minimum put a compiling tree below a failing one
+/// in 71 of 240 pairs, this width in 193.
+fn cut_width(ctx_in: u32, cross: u32, clause_count: u64) -> f64 {
+    f64::from(cross) * f64::from(ctx_in) / clause_count.max(1) as f64
+}
+
 fn separator_terms(
     vtree: &Vtree,
     ctx_in: &[u32],
     ctx_out: &[u32],
     cross: &[u32],
+    clause_count: u64,
 ) -> (f64, f64, f64, Vec<u32>) {
     let mut tight_widths = vec![0u32; vtree.num_nodes()];
     let mut second = vec![0u32; vtree.num_nodes()];
     let mut cross_width = vec![0u32; vtree.num_nodes()];
+    let mut width = vec![0f64; vtree.num_nodes()];
     for t in vtree.bottomup() {
         let i = t.idx();
         let mut bounds = [ctx_in[i], ctx_out[i], cross[i]];
@@ -231,24 +251,34 @@ fn separator_terms(
         tight_widths[i] = bounds[0].min(leaf_cap);
         second[i] = bounds[1].min(leaf_cap);
         cross_width[i] = cross[i].min(leaf_cap);
+        width[i] = if vtree.node(t).is_leaf() {
+            f64::from(tight_widths[i])
+        } else {
+            cut_width(ctx_in[i], cross[i], clause_count)
+        };
     }
 
     let mut tight_terms = Vec::with_capacity(vtree.num_nodes() / 2);
+    let mut bound_terms = Vec::with_capacity(vtree.num_nodes() / 2);
     let mut capped_terms = Vec::with_capacity(vtree.num_nodes() / 2);
     let mut pair_cross_terms = Vec::with_capacity(vtree.num_nodes() / 2);
     let mut out_terms = Vec::with_capacity(vtree.num_nodes() / 2);
     for (t, left, right) in vtree.internal_bottomup() {
         let i = t.idx();
-        tight_terms.push(f64::from(tight_widths[i]));
+        tight_terms.push(width[i]);
+        bound_terms.push(f64::from(tight_widths[i]));
         capped_terms
             .push(f64::from(tight_widths[i]) + f64::from((second[i] - tight_widths[i]).min(7)));
         pair_cross_terms
             .push(f64::from(cross_width[left.idx()]) + f64::from(cross_width[right.idx()]));
         out_terms.push(f64::from(ctx_out[i]));
     }
     let tight = log2_sum_exp(&tight_terms);
-    let capped_gap = (log2_sum_exp(&capped_terms) - tight).max(0.0);
-    let pair_cross_gap = (log2_sum_exp(&pair_cross_terms) - tight).max(0.0);
+    // The excess term is the gap between the smallest and the second-smallest
+    // of the three bounds, so it is measured against the sum of the smallest.
+    let tight_bound = log2_sum_exp(&bound_terms);
+    let capped_gap = (log2_sum_exp(&capped_terms) - tight_bound).max(0.0);
+    let pair_cross_gap = (log2_sum_exp(&pair_cross_terms) - tight_bound).max(0.0);
     let excess = (capped_gap - (1.0 + pair_cross_gap).log2()).max(0.0);
     (tight, excess, log2_sum_exp(&out_terms), tight_widths)
 }
@@ -556,8 +586,14 @@ fn unified_cost_from_tables(
     load_stddev: f64,
     depth: u32,
 ) -> f64 {
-    let (tight, excess, outside, tight_widths) =
-        separator_terms(vtree, tables.ctx_in, tables.ctx_out, tables.cross);
+    let clause_count: u64 = tables.clause_at.iter().map(|&load| u64::from(load)).sum();
+    let (tight, excess, outside, tight_widths) = separator_terms(
+        vtree,
+        tables.ctx_in,
+        tables.ctx_out,
+        tables.cross,
+        clause_count,
+    );
     if tight == 0.0 {
         return 0.0;
     }
@@ -567,7 +603,6 @@ fn unified_cost_from_tables(
     let leaves = f64::from(vtree.num_leaves());
     let chain = (1.0 + (5.0 * f64::from(depth) - leaves - 1.0).max(0.0)).log2();
     let high_load = (1.0 + load_stddev).log2() * (tight - 16.0).max(0.0);
-    let clause_count: u64 = tables.clause_at.iter().map(|&load| u64::from(load)).sum();
     let shallow = 5 * u64::from(depth) <= u64::from(vtree.num_leaves()) + 1;
     let needs_matching = vtree.internal_bottomup().any(|(node, _, _)| {
         let load = f64::from(tables.clause_at[node.idx()]);

src/tests/score.rs

@@ -24,9 +24,11 @@ use crate::vtree::VarId;
 ///   `R` — `A` for v0 and v1, `B` for v2 and v3. Both cuts are 2 wide.
 /// * `peak_context_width_show` with only v0 and v2 shown counts one crossing at `A` and
 ///   one at `B`, so 1.
-/// * `cost`: the separator term is `log₂(2² + 2²) = 3`; the clause-load
-///   cost is 17; the depth term is `log₂(6)`; the successor guards add 3.
-///   combined result is `6 + 9 log₂(18)/5 + 3 log₂(6)/40`.
+/// * `cost`: each of the two cuts carries two of the five clauses over two
+///   inside variables, a width of `2 · 2 / 5`, so the separator term is
+///   `log₂(2^0.8 + 2^0.8) = 1.8`; the clause-load cost is 17; the depth term
+///   is `log₂(6)`; the successor guards add 3. The combined result is
+///   `4.8 + 9 log₂(18)/5 + 3 log₂(6)/40`.
 #[test]
 fn fixture_metrics_match_hand_computation() {
     let formula = fixture_formula();
@@ -46,7 +48,7 @@ fn fixture_metrics_match_hand_computation() {
         Some(1),
         "peak_context_width_show"
     );
-    let expected_cost = 6.0 + 9.0 * 18.0f64.log2() / 5.0 + 3.0 * 6.0f64.log2() / 40.0;
+    let expected_cost = 4.8 + 9.0 * 18.0f64.log2() / 5.0 + 3.0 * 6.0f64.log2() / 40.0;
     assert!(
         (stats.cost - expected_cost).abs() < 1e-12,
         "cost: {}",