Add complexity consistency audit; fix NonTautology, MinimumWeightDecoding and MaxCut<One> complexities

docs/paper/reductions.typ

@@ -5729,7 +5729,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
     #problem-def("NonTautology")[
       Given a Boolean formula in DNF $phi = or.big_(j=1)^m D_j$ with $m$ disjuncts over $n$ Boolean variables, where each disjunct $D_j$ is a conjunction of literals, find a truth assignment $bold(x) in {0, 1}^n$ such that $phi(bold(x)) = 0$ (i.e., every disjunct is false).
     ][
-    The Non-Tautology problem asks whether a given DNF formula is _not_ a tautology, by finding a falsifying assignment. A disjunct $D_j = ell_1 and dots and ell_k$ is false when at least one of its literals evaluates to false; the formula is false when all disjuncts are false. The problem is coNP-complete in general and closely related to SAT through De Morgan duality: a DNF formula $phi$ is a tautology iff $not phi$ (a CNF formula) is unsatisfiable.
+    The Non-Tautology problem asks whether a given DNF formula is _not_ a tautology, by finding a falsifying assignment. A disjunct $D_j = ell_1 and dots and ell_k$ is false when at least one of its literals evaluates to false; the formula is false when all disjuncts are false. The problem is NP-complete in general and closely related to SAT through De Morgan duality: a DNF formula $phi$ is a tautology iff $not phi$ (a CNF formula) is unsatisfiable. Because disjunct width is unbounded, this duality makes it as hard as CNF-SAT: no $O^*((2-epsilon)^n)$ algorithm is known (SETH) @impagliazzo2001, and we register $O^*(2^n)$.
 
     *Example.* Consider $phi = #disjuncts.map(fmt-disjunct).join($or$)$ with $n = #n$ variables and $m = #m$ disjuncts. The assignment $(#range(n).map(i => $x_#(i + 1)$).join(",")) = (#fmt-values(assign))$ falsifies the formula: #disjuncts.enumerate().map(((j, d)) => $D_#(j + 1)$+ " is " + if disjunct-true(d) { "true" } else { "false" }).join(", ").
 
@@ -10992,7 +10992,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
     ][
       Minimum Weight Decoding is a fundamental problem in coding theory. Given a linear code with parity-check matrix $H$, the task is to find the minimum-weight error pattern consistent with a received syndrome. The problem is equivalent to finding the closest codeword to a received word and is central to the hardness of decoding random linear codes.
 
-      The best known algorithms for general instances use information set decoding techniques, achieving $O(2^(0.0494 n))$ where $n$ is the block length.
+      Information set decoding achieves much smaller exponents on average over random codes, but these do not bound worst-case instances. For worst-case instances, split the $m$ columns of $H$ into $L$ of size $floor(m slash 2)$ and $R$ of size $ceil(m slash 2)$. For each $x_L in {0,1}^(floor(m slash 2))$, store the lightest $x_L$ under the key $H_L x_L$; then for each $x_R$, look up the key $s + H_R x_R$. This meet-in-the-middle search is exact and runs in $O^*(2^(ceil(m slash 2)))$ time and $O^*(2^(floor(m slash 2)))$ space. In terms of the rank $k = m - "rank"(H)$ of the solution coset $x_0 + ker H$, exhaustive search takes $O^*(2^k)$ time, and no $O^*(2^((1-epsilon) k))$ algorithm exists unless SETH fails @stephensdavidowitz2019seth.
 
       *Example.* Let $H$ be the #(n)$times$#(m) binary matrix and $s = (#fmt-values(s))$. The optimal config $(#fmt-values(cfg))$ has Hamming weight $#wt$.
 

docs/paper/references.bib

@@ -984,6 +984,15 @@ @inproceedings{aggarwal2015
   doi       = {10.1109/FOCS.2015.41}
 }
 
+@inproceedings{stephensdavidowitz2019seth,
+  author    = {Noah Stephens-Davidowitz and Vinod Vaikuntanathan},
+  title     = {{SETH}-Hardness of Coding Problems},
+  booktitle = {Proceedings of the 60th Annual Symposium on Foundations of Computer Science (FOCS)},
+  pages     = {287--301},
+  year      = {2019},
+  doi       = {10.1109/FOCS.2019.00027}
+}
+
 @inproceedings{razgon2007,
   author    = {Igor Razgon},
   title     = {Computing Minimum Directed Feedback Vertex Set in {$O^*(1.9977^n)$}},

examples/complexity_consistency_audit.rs

@@ -0,0 +1,201 @@
+//! Audit registered variant complexities against the reduction graph.
+//!
+//! For every simple path A -> ... -> B of 1-3 witness hops, substitute the
+//! path's composed parameter transform into B's registered complexity. The
+//! resulting expression is a candidate bound on solving A. Substitution of
+//! upper-bound parameters requires the target complexity to be monotone in those
+//! parameters; a known growth form alone does not prove that property.
+//! The audit compares represented growth bounds and reports the shortest route
+//! for each candidate improvement. Widening can make a registered bound loose,
+//! and the reduction's own running time is not modeled. Every finding therefore
+//! requires manual verification of monotonicity, tightness, and reduction cost.
+//!
+//! cargo run --release --example complexity_consistency_audit
+use problemreductions::Growth;
+use problemreductions::expr::Expr;
+use problemreductions::rules::{ReductionGraph, ReductionPath, ReductionStep};
+use std::collections::{BTreeMap, HashMap};
+
+const MAX_HOPS: usize = 3;
+
+type Node = (String, BTreeMap<String, String>);
+
+struct Finding {
+    path: ReductionPath,
+    registered: String,
+    derived: String,
+    target_complexity: String,
+}
+
+#[derive(Default)]
+struct Totals {
+    paths: usize,
+    no_complexity: usize,
+    uncomposable: usize,
+    unknown_growth: usize,
+    incomparable: usize,
+    consistent: usize,
+    violations: usize,
+    unknown_reasons: BTreeMap<String, usize>,
+}
+
+fn extend(graph: &ReductionGraph, path: &mut Vec<Node>, found: &mut Vec<ReductionPath>) {
+    if path.len() > MAX_HOPS {
+        return;
+    }
+    let (name, variant) = path.last().expect("non-empty path").clone();
+    for edge in graph.outgoing_reductions(&name) {
+        // Aggregate-only edges bound a value, not a witness search.
+        if edge.source_variant != variant || edge.capabilities.turing || !edge.capabilities.witness
+        {
+            continue;
+        }
+        let next = (edge.target_name.to_string(), edge.target_variant);
+        if path.contains(&next) {
+            continue;
+        }
+        path.push(next);
+        found.push(ReductionPath {
+            steps: path
+                .iter()
+                .map(|(name, variant)| ReductionStep {
+                    name: name.clone(),
+                    variant: variant.clone(),
+                })
+                .collect(),
+        });
+        extend(graph, path, found);
+        path.pop();
+    }
+}
+
+/// The target complexity rewritten in source parameters, if every step composes.
+///
+/// Substituting upper-bound fields is sound only for a complexity that is
+/// monotone in the substituted parameters. The caller skips unsupported target
+/// growth forms, but support is not a monotonicity proof. Findings must be
+/// checked against the target formula and each transform's accuracy.
+fn derived_complexity(graph: &ReductionGraph, path: &ReductionPath, target: &str) -> Option<Expr> {
+    let composed = graph.compose_path_parameter_transform(path).ok()??;
+    let replacements: HashMap<&str, &Expr> = composed.expressions().collect();
+    Expr::parse(target).substitute_complete(&replacements).ok()
+}
+
+fn label(step: &ReductionStep) -> String {
+    let variant: Vec<&str> = step.variant.values().map(String::as_str).collect();
+    if variant.is_empty() {
+        step.name.clone()
+    } else {
+        format!("{}/{}", step.name, variant.join("/"))
+    }
+}
+
+fn main() {
+    let graph = ReductionGraph::new();
+    let mut paths = Vec::new();
+    for name in graph.problem_types() {
+        for variant in graph.variants_for(name) {
+            extend(&graph, &mut vec![(name.to_string(), variant)], &mut paths);
+        }
+    }
+
+    let mut totals = Totals::default();
+    let mut findings: BTreeMap<String, Vec<Finding>> = BTreeMap::new();
+    for path in paths {
+        totals.paths += 1;
+        let (first, last) = (
+            &path.steps[0],
+            path.steps.last().expect("path has a target"),
+        );
+        let (Some(registered), Some(target)) = (
+            graph.variant_complexity(&first.name, &first.variant),
+            graph.variant_complexity(&last.name, &last.variant),
+        ) else {
+            totals.no_complexity += 1;
+            continue;
+        };
+        if Growth::from_expr(&Expr::parse(target)).failures().is_some() {
+            totals.unknown_growth += 1;
+            *totals
+                .unknown_reasons
+                .entry("target complexity unsupported".into())
+                .or_default() += 1;
+            continue;
+        }
+        let Some(derived) = derived_complexity(&graph, &path, target) else {
+            totals.uncomposable += 1;
+            continue;
+        };
+        let derived_growth = Growth::from_expr(&derived);
+        let registered_growth = Growth::from_expr(&Expr::parse(registered));
+        let failure = derived_growth
+            .failures()
+            .map(|failures| ("derived", failures))
+            .or_else(|| {
+                registered_growth
+                    .failures()
+                    .map(|failures| ("registered", failures))
+            });
+        if let Some((side, failures)) = failure {
+            totals.unknown_growth += 1;
+            for failure in failures {
+                let kind = failure.to_string();
+                let kind = kind.split(':').next().unwrap_or_default();
+                *totals
+                    .unknown_reasons
+                    .entry(format!("{side}: {kind}"))
+                    .or_default() += 1;
+            }
+            continue;
+        }
+        let derived_dominates = derived_growth.dominates(&registered_growth);
+        let registered_dominates = registered_growth.dominates(&derived_growth);
+        match (registered_dominates, derived_dominates) {
+            (true, false) => {
+                totals.violations += 1;
+                let derived_big_o = derived_growth.to_big_o();
+                findings.entry(label(first)).or_default().push(Finding {
+                    path,
+                    registered: registered.to_string(),
+                    derived: derived_big_o,
+                    target_complexity: target.to_string(),
+                });
+            }
+            (false, false) => totals.incomparable += 1,
+            _ => totals.consistent += 1,
+        }
+    }
+
+    println!("Complexity consistency audit (paths of 1-{MAX_HOPS} witness hops)");
+    println!("paths examined:        {}", totals.paths);
+    println!("  consistent:          {}", totals.consistent);
+    println!("  candidate improvements:   {}", totals.violations);
+    println!("  incomparable Big-O:  {}", totals.incomparable);
+    println!("  unknown growth:      {}", totals.unknown_growth);
+    println!("  uncomposable:        {}", totals.uncomposable);
+    println!("  no complexity:       {}", totals.no_complexity);
+    for (reason, count) in &totals.unknown_reasons {
+        println!("    unknown growth, {reason}: {count}");
+    }
+
+    println!(
+        "\n## Candidate improvements requiring manual review ({} variants)",
+        findings.len()
+    );
+    for (source, list) in &findings {
+        let best = list
+            .iter()
+            .min_by_key(|f| f.path.steps.len())
+            .expect("non-empty finding list");
+        let route: Vec<String> = best.path.steps.iter().map(label).collect();
+        println!("- {source}");
+        println!("    registered: {}", best.registered);
+        println!(
+            "    derived:    {}  ({} witness paths)",
+            best.derived,
+            list.len()
+        );
+        println!("    via:        {}", route.join(" -> "));
+        println!("    target:     {}", best.target_complexity);
+    }
+}

src/models/algebraic/minimum_weight_decoding.rs

@@ -179,7 +179,9 @@ impl crate::solvers::BruteForceProblem for MinimumWeightDecoding {
 }
 
 crate::declare_variants! {
-    default MinimumWeightDecoding => "2^(0.0494 * num_cols)" create MinimumWeightDecodingCreateSpec,
+    // Information set decoding exponents are average-case over random codes. Worst case:
+    // meet-in-the-middle over the two column halves of H is exact in 2^(m/2).
+    default MinimumWeightDecoding => "2^(0.5 * num_cols)" create MinimumWeightDecodingCreateSpec,
 }
 
 crate::register_brute_force! {

src/models/formula/non_tautology.rs

@@ -179,7 +179,8 @@ impl crate::solvers::BruteForceProblem for NonTautology {
 }
 
 crate::declare_variants! {
-    default NonTautology => "1.307^num_vars",
+    // Unbounded-width DNF is CNF-SAT by De Morgan duality; no O*((2-eps)^n) algorithm is known.
+    default NonTautology => "2^num_vars",
 }
 
 crate::register_brute_force! {

src/models/graph/max_cut.rs

@@ -289,7 +289,7 @@ crate::impl_random_generate!(MaxCut<SimpleGraph, i64>, crate::random::SimpleGrap
 
 crate::declare_variants! {
     default MaxCut<SimpleGraph, i64> => "2^(2.372 * num_vertices / 3)" create MaxCutI64CreateSpec random,
-    MaxCut<SimpleGraph, One> => "2^(0.7907 * num_vertices)" create MaxCutOneCreateSpec,
+    MaxCut<SimpleGraph, One> => "2^(2.372 * num_vertices / 3)" create MaxCutOneCreateSpec,
 }
 
 crate::register_brute_force! {

src/unit_tests/models/algebraic/minimum_weight_decoding.rs

@@ -154,7 +154,7 @@ fn test_minimum_weight_decoding_complexity_metadata() {
         .find(|entry| entry.name == "MinimumWeightDecoding")
         .expect("MinimumWeightDecoding variant entry should exist");
 
-    assert_eq!(entry.complexity, "2^(0.0494 * num_cols)");
+    assert_eq!(entry.complexity, "2^(0.5 * num_cols)");
 }
 
 #[test]