From 81b4f23612347a7cc5fa9ebbf43bda94537938e0 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Tue, 27 Oct 2026 03:05:28 -0700 Subject: [PATCH 1/6] Add complexity consistency audit and fix two wrong complexity entries The audit substitutes each reduction path's composed parameter transform into the target's registered complexity and flags sources whose registered bound is beaten by the derived one. It surfaced two wrong entries: - NonTautology claimed the 3-SAT bound 1.307^n, but unbounded-width DNF is CNF-SAT by De Morgan duality; best known is 2^n. - MinimumWeightDecoding claimed 2^(0.0494 m), an average-case exponent for random codes; no worst-case bound below exhaustive search is known. Co-Authored-By: Claude Opus 5.5 --- docs/paper/reductions.typ | 4 +- examples/complexity_consistency_audit.rs | 204 ++++++++++++++++++ .../algebraic/minimum_weight_decoding.rs | 4 +- src/models/formula/non_tautology.rs | 3 +- .../algebraic/minimum_weight_decoding.rs | 2 +- 5 files changed, 212 insertions(+), 5 deletions(-) create mode 100644 examples/complexity_consistency_audit.rs diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 44256b45b..8e711a215 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -5702,7 +5702,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 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. Because disjunct width is unbounded, this duality makes it as hard as CNF-SAT, so the best known algorithm is $O^*(2^n)$ exhaustive search. *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(", "). @@ -10965,7 +10965,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. In the worst case no algorithm is known beyond enumerating the solution coset $x_0 + ker H$, which takes $O^*(2^(m - "rank"(H))) subset.eq O^*(2^m)$ time. *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$. diff --git a/examples/complexity_consistency_audit.rs b/examples/complexity_consistency_audit.rs new file mode 100644 index 000000000..7de790037 --- /dev/null +++ b/examples/complexity_consistency_audit.rs @@ -0,0 +1,204 @@ +//! Audit registered variant complexities against the reduction graph. +//! +//! For every simple path A -> ... -> B of 1-3 non-Turing hops, substitute the +//! path's composed parameter transform into B's registered complexity. The +//! result is an upper bound on solving A (plus the polynomial reduction cost). +//! When that derived bound is strictly smaller in Big-O than A's registered +//! complexity, either A's entry is stale or a transform along the path is +//! wrong; the audit reports the shortest such witness for each variant. +//! +//! Findings where both bounds are polynomial are listed separately: the +//! reduction's own running time is not modeled, so they are only suggestive. +//! +//! cargo run --release --example complexity_consistency_audit +use problemreductions::expr::Expr; +use problemreductions::rules::{ReductionGraph, ReductionPath, ReductionStep}; +use problemreductions::Growth; +use std::collections::{BTreeMap, HashMap}; + +const MAX_HOPS: usize = 3; + +type Node = (String, BTreeMap); + +struct Finding { + path: ReductionPath, + registered: String, + derived: String, + target_complexity: String, + polynomial: bool, +} + +#[derive(Default)] +struct Totals { + paths: usize, + uncomposable: usize, + unknown_growth: usize, + incomparable: usize, + consistent: usize, + violations: usize, + unknown_reasons: BTreeMap, +} + +fn extend(graph: &ReductionGraph, path: &mut Vec, found: &mut Vec) { + if path.len() > MAX_HOPS { + return; + } + let (name, variant) = path.last().expect("non-empty path").clone(); + for edge in graph.outgoing_reductions(&name) { + if edge.source_variant != variant || edge.capabilities.turing { + 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. +/// Both exact and upper-bound fields are sound inputs: complexities are monotone. +fn derived_complexity(graph: &ReductionGraph, path: &ReductionPath, target: &str) -> Option { + let composed = graph.compose_path_parameter_transform(path).ok()??; + let replacements: HashMap<&str, &Expr> = composed.expressions().collect(); + Expr::parse(target).substitute_complete(&replacements).ok() +} + +/// Polynomial iff every exponent is a numeric literal. +fn is_polynomial(expr: &Expr) -> bool { + expr.to_string().split('^').skip(1).all(|exponent| { + exponent + .trim_start() + .starts_with(|c: char| c.is_ascii_digit()) + }) +} + +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> = 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.uncomposable += 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)); + if let Some(failures) = derived_growth.failures().or(registered_growth.failures()) { + totals.unknown_growth += 1; + let side = if registered_growth.failures().is_some() { + "registered" + } else { + "derived" + }; + 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(®istered_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 { + polynomial: is_polynomial(&Expr::parse(registered)), + 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} non-Turing hops)"); + println!("paths examined: {}", totals.paths); + println!(" consistent: {}", totals.consistent); + println!(" derived is better: {}", totals.violations); + println!(" incomparable Big-O: {}", totals.incomparable); + println!(" unknown growth: {}", totals.unknown_growth); + println!(" uncomposable: {}", totals.uncomposable); + for (reason, count) in &totals.unknown_reasons { + println!(" unknown growth, {reason}: {count}"); + } + + let (polynomial, exponential): (Vec<_>, Vec<_>) = findings + .iter() + .map(|(source, list)| { + let best = list + .iter() + .min_by_key(|f| f.path.steps.len()) + .expect("non-empty finding list"); + (source, list.len(), best) + }) + .partition(|(_, _, best)| best.polynomial); + + for (title, group) in [ + ( + "Exponential registered bound beaten by a derived bound", + exponential, + ), + ( + "Polynomial registered bound beaten (reduction cost not modeled)", + polynomial, + ), + ] { + println!("\n## {title} ({} variants)", group.len()); + for (source, count, best) in group { + let route: Vec = best.path.steps.iter().map(label).collect(); + println!("- {source}"); + println!(" registered: {}", best.registered); + println!(" derived: {} ({count} witness paths)", best.derived); + println!(" via: {}", route.join(" -> ")); + println!(" target: {}", best.target_complexity); + } + } +} diff --git a/src/models/algebraic/minimum_weight_decoding.rs b/src/models/algebraic/minimum_weight_decoding.rs index 5c9c4b283..caed0fa74 100644 --- a/src/models/algebraic/minimum_weight_decoding.rs +++ b/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; no + // worst-case bound below exhaustive search over x is known. + default MinimumWeightDecoding => "2^num_cols" create MinimumWeightDecodingCreateSpec, } crate::register_brute_force! { diff --git a/src/models/formula/non_tautology.rs b/src/models/formula/non_tautology.rs index a45f40aab..36de1ae1c 100644 --- a/src/models/formula/non_tautology.rs +++ b/src/models/formula/non_tautology.rs @@ -183,7 +183,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! { diff --git a/src/unit_tests/models/algebraic/minimum_weight_decoding.rs b/src/unit_tests/models/algebraic/minimum_weight_decoding.rs index 20947b66a..6445f979c 100644 --- a/src/unit_tests/models/algebraic/minimum_weight_decoding.rs +++ b/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^num_cols"); } #[test] From ea882aae742ed4585a73c6679f9ad22596484728 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Tue, 27 Oct 2026 03:32:21 -0700 Subject: [PATCH 2/6] Address review: tighten MinimumWeightDecoding bound and harden the audit - MinimumWeightDecoding: register 2^(0.773 m). A consistent system has a solution of weight <= rank(H); the cheaper of coset and low-weight enumeration balances at r/m ~ 0.2271. Derivation added to the paper. - NonTautology paper text: state the SETH barrier instead of claiming exhaustive search is best known. - Audit: skip aggregate-only edges, skip targets whose complexity the growth domain cannot analyze before substituting, count missing complexities separately, and drop the string-based polynomial split. Co-Authored-By: Claude Opus 5.5 --- docs/paper/reductions.typ | 4 +- examples/complexity_consistency_audit.rs | 90 +++++++++---------- .../algebraic/minimum_weight_decoding.rs | 7 +- .../algebraic/minimum_weight_decoding.rs | 2 +- 4 files changed, 49 insertions(+), 54 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 8e711a215..badf33100 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -5702,7 +5702,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. Because disjunct width is unbounded, this duality makes it as hard as CNF-SAT, so the best known algorithm is $O^*(2^n)$ exhaustive search. + 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. Because disjunct width is unbounded, this duality makes it as hard as CNF-SAT: no $O^*((2-epsilon)^n)$ algorithm is known (SETH), 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(", "). @@ -10965,7 +10965,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. - Information set decoding achieves much smaller exponents on average over random codes, but these do not bound worst-case instances. In the worst case no algorithm is known beyond enumerating the solution coset $x_0 + ker H$, which takes $O^*(2^(m - "rank"(H))) subset.eq O^*(2^m)$ time. + Information set decoding achieves much smaller exponents on average over random codes, but these do not bound worst-case instances. For worst-case instances, let $r = "rank"(H)$. A consistent system has a solution supported on $r$ linearly independent columns, so the optimum has weight at most $r$. Taking the cheaper of enumerating the solution coset $x_0 + ker H$ in $O^*(2^(m - r))$ time and enumerating all $x$ of weight at most $r$ in $O^*(2^(m h(r slash m)))$ time, where $h$ is the binary entropy function, gives $O^*(2^(0.773 m))$ for every $r$; the two costs balance at $r slash m approx 0.2271$. *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$. diff --git a/examples/complexity_consistency_audit.rs b/examples/complexity_consistency_audit.rs index 7de790037..bbf1aa26f 100644 --- a/examples/complexity_consistency_audit.rs +++ b/examples/complexity_consistency_audit.rs @@ -1,14 +1,14 @@ //! Audit registered variant complexities against the reduction graph. //! -//! For every simple path A -> ... -> B of 1-3 non-Turing hops, substitute the +//! For every simple path A -> ... -> B of 1-3 witness hops, substitute the //! path's composed parameter transform into B's registered complexity. The //! result is an upper bound on solving A (plus the polynomial reduction cost). //! When that derived bound is strictly smaller in Big-O than A's registered //! complexity, either A's entry is stale or a transform along the path is //! wrong; the audit reports the shortest such witness for each variant. //! -//! Findings where both bounds are polynomial are listed separately: the -//! reduction's own running time is not modeled, so they are only suggestive. +//! The reduction's own running time is not modeled, so a finding whose +//! registered bound is polynomial is only suggestive. //! //! cargo run --release --example complexity_consistency_audit use problemreductions::expr::Expr; @@ -25,12 +25,12 @@ struct Finding { registered: String, derived: String, target_complexity: String, - polynomial: bool, } #[derive(Default)] struct Totals { paths: usize, + no_complexity: usize, uncomposable: usize, unknown_growth: usize, incomparable: usize, @@ -45,7 +45,9 @@ fn extend(graph: &ReductionGraph, path: &mut Vec, found: &mut Vec, found: &mut Vec Option { let composed = graph.compose_path_parameter_transform(path).ok()??; let replacements: HashMap<&str, &Expr> = composed.expressions().collect(); Expr::parse(target).substitute_complete(&replacements).ok() } -/// Polynomial iff every exponent is a numeric literal. -fn is_polynomial(expr: &Expr) -> bool { - expr.to_string().split('^').skip(1).all(|exponent| { - exponent - .trim_start() - .starts_with(|c: char| c.is_ascii_digit()) - }) -} - fn label(step: &ReductionStep) -> String { let variant: Vec<&str> = step.variant.values().map(String::as_str).collect(); if variant.is_empty() { @@ -114,9 +111,17 @@ fn main() { graph.variant_complexity(&first.name, &first.variant), graph.variant_complexity(&last.name, &last.variant), ) else { - totals.uncomposable += 1; + 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; @@ -147,7 +152,6 @@ fn main() { totals.violations += 1; let derived_big_o = derived_growth.to_big_o(); findings.entry(label(first)).or_default().push(Finding { - polynomial: is_polynomial(&Expr::parse(registered)), path, registered: registered.to_string(), derived: derived_big_o, @@ -159,46 +163,36 @@ fn main() { } } - println!("Complexity consistency audit (paths of 1-{MAX_HOPS} non-Turing hops)"); + println!("Complexity consistency audit (paths of 1-{MAX_HOPS} witness hops)"); println!("paths examined: {}", totals.paths); println!(" consistent: {}", totals.consistent); println!(" derived is better: {}", 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}"); } - let (polynomial, exponential): (Vec<_>, Vec<_>) = findings - .iter() - .map(|(source, list)| { - let best = list - .iter() - .min_by_key(|f| f.path.steps.len()) - .expect("non-empty finding list"); - (source, list.len(), best) - }) - .partition(|(_, _, best)| best.polynomial); - - for (title, group) in [ - ( - "Exponential registered bound beaten by a derived bound", - exponential, - ), - ( - "Polynomial registered bound beaten (reduction cost not modeled)", - polynomial, - ), - ] { - println!("\n## {title} ({} variants)", group.len()); - for (source, count, best) in group { - let route: Vec = best.path.steps.iter().map(label).collect(); - println!("- {source}"); - println!(" registered: {}", best.registered); - println!(" derived: {} ({count} witness paths)", best.derived); - println!(" via: {}", route.join(" -> ")); - println!(" target: {}", best.target_complexity); - } + println!( + "\n## Registered bound beaten by a derived bound ({} 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 = 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); } } diff --git a/src/models/algebraic/minimum_weight_decoding.rs b/src/models/algebraic/minimum_weight_decoding.rs index caed0fa74..275d779ef 100644 --- a/src/models/algebraic/minimum_weight_decoding.rs +++ b/src/models/algebraic/minimum_weight_decoding.rs @@ -179,9 +179,10 @@ impl crate::solvers::BruteForceProblem for MinimumWeightDecoding { } crate::declare_variants! { - // Information set decoding exponents are average-case over random codes; no - // worst-case bound below exhaustive search over x is known. - default MinimumWeightDecoding => "2^num_cols" create MinimumWeightDecodingCreateSpec, + // Information set decoding exponents are average-case over random codes. Worst case: + // the cheaper of coset enumeration, 2^(m - r), and weight-<=r enumeration, + // 2^(m h(r/m)) for binary entropy h, with r = rank(H); the two balance at r/m ~ 0.2271. + default MinimumWeightDecoding => "2^(0.773 * num_cols)" create MinimumWeightDecodingCreateSpec, } crate::register_brute_force! { diff --git a/src/unit_tests/models/algebraic/minimum_weight_decoding.rs b/src/unit_tests/models/algebraic/minimum_weight_decoding.rs index 6445f979c..578f79dff 100644 --- a/src/unit_tests/models/algebraic/minimum_weight_decoding.rs +++ b/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^num_cols"); + assert_eq!(entry.complexity, "2^(0.773 * num_cols)"); } #[test] From 635d7257bc3589c8fae70c46c720bfffea32009e Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Thu, 29 Oct 2026 02:04:07 -0700 Subject: [PATCH 3/6] Fix import order for Rust 2024 rustfmt Co-Authored-By: Claude Opus 5.5 --- examples/complexity_consistency_audit.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/complexity_consistency_audit.rs b/examples/complexity_consistency_audit.rs index bbf1aa26f..7387b290e 100644 --- a/examples/complexity_consistency_audit.rs +++ b/examples/complexity_consistency_audit.rs @@ -11,9 +11,9 @@ //! registered bound is polynomial is only suggestive. //! //! cargo run --release --example complexity_consistency_audit +use problemreductions::Growth; use problemreductions::expr::Expr; use problemreductions::rules::{ReductionGraph, ReductionPath, ReductionStep}; -use problemreductions::Growth; use std::collections::{BTreeMap, HashMap}; const MAX_HOPS: usize = 3; From 2892ae57fcfcf9299329198f0934fb4c2aa7135a Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Thu, 29 Oct 2026 02:09:14 -0700 Subject: [PATCH 4/6] Write MaxCut complexity in the same form as MaxCut 0.7907 rounded 2.372/3 = 0.79067 up, so the audit flagged the One variant as beaten by its own i64 variant. Co-Authored-By: Claude Opus 5.5 --- src/models/graph/max_cut.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/models/graph/max_cut.rs b/src/models/graph/max_cut.rs index 286f0efb6..b28b64d7a 100644 --- a/src/models/graph/max_cut.rs +++ b/src/models/graph/max_cut.rs @@ -289,7 +289,7 @@ crate::impl_random_generate!(MaxCut, crate::random::SimpleGrap crate::declare_variants! { default MaxCut => "2^(2.372 * num_vertices / 3)" create MaxCutI64CreateSpec random, - MaxCut => "2^(0.7907 * num_vertices)" create MaxCutOneCreateSpec, + MaxCut => "2^(2.372 * num_vertices / 3)" create MaxCutOneCreateSpec, } crate::register_brute_force! { From c89e6ea40232543d2617f92193f61a5140cafed4 Mon Sep 17 00:00:00 2001 From: Xiwei Pan <90967972+isPANN@users.noreply.github.com> Date: Thu, 29 Oct 2026 02:24:42 -0700 Subject: [PATCH 5/6] Register meet-in-the-middle 2^(m/2) for MinimumWeightDecoding Splitting the columns of H into halves and matching H_L x_L against s + H_R x_R is exact and beats the 2^(0.773 m) rank argument on every instance. The paper now cites Stephens-Davidowitz and Vaikuntanathan (FOCS 2019) for SETH-optimality of 2^k in the coset rank k. Co-Authored-By: Claude Opus 5.5 --- docs/paper/reductions.typ | 2 +- docs/paper/references.bib | 9 +++++++++ src/models/algebraic/minimum_weight_decoding.rs | 5 ++--- .../models/algebraic/minimum_weight_decoding.rs | 2 +- 4 files changed, 13 insertions(+), 5 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 2c4d7f5d3..0522bf31b 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -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. - Information set decoding achieves much smaller exponents on average over random codes, but these do not bound worst-case instances. For worst-case instances, let $r = "rank"(H)$. A consistent system has a solution supported on $r$ linearly independent columns, so the optimum has weight at most $r$. Taking the cheaper of enumerating the solution coset $x_0 + ker H$ in $O^*(2^(m - r))$ time and enumerating all $x$ of weight at most $r$ in $O^*(2^(m h(r slash m)))$ time, where $h$ is the binary entropy function, gives $O^*(2^(0.773 m))$ for every $r$; the two costs balance at $r slash m approx 0.2271$. + 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 halves $L$ and $R$. For each $x_L in {0,1}^(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^(m slash 2))$ time. 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$. diff --git a/docs/paper/references.bib b/docs/paper/references.bib index 640774531..0dda81fd2 100644 --- a/docs/paper/references.bib +++ b/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)$}}, diff --git a/src/models/algebraic/minimum_weight_decoding.rs b/src/models/algebraic/minimum_weight_decoding.rs index 249c7c3c0..e3d9ce83b 100644 --- a/src/models/algebraic/minimum_weight_decoding.rs +++ b/src/models/algebraic/minimum_weight_decoding.rs @@ -180,9 +180,8 @@ impl crate::solvers::BruteForceProblem for MinimumWeightDecoding { crate::declare_variants! { // Information set decoding exponents are average-case over random codes. Worst case: - // the cheaper of coset enumeration, 2^(m - r), and weight-<=r enumeration, - // 2^(m h(r/m)) for binary entropy h, with r = rank(H); the two balance at r/m ~ 0.2271. - default MinimumWeightDecoding => "2^(0.773 * num_cols)" create MinimumWeightDecodingCreateSpec, + // 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! { diff --git a/src/unit_tests/models/algebraic/minimum_weight_decoding.rs b/src/unit_tests/models/algebraic/minimum_weight_decoding.rs index b193a7361..2e14a611c 100644 --- a/src/unit_tests/models/algebraic/minimum_weight_decoding.rs +++ b/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.773 * num_cols)"); + assert_eq!(entry.complexity, "2^(0.5 * num_cols)"); } #[test] From 22b3c0b9eae0add3ca242cc37a93519365e57327 Mon Sep 17 00:00:00 2001 From: GiggleLiu Date: Fri, 30 Oct 2026 14:43:31 +0800 Subject: [PATCH 6/6] Clarify audit guarantees and decoding resource bounds --- docs/paper/reductions.typ | 4 +-- examples/complexity_consistency_audit.rs | 39 +++++++++++++----------- 2 files changed, 23 insertions(+), 20 deletions(-) diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 0522bf31b..8e0462b7a 100644 --- a/docs/paper/reductions.typ +++ b/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. Because disjunct width is unbounded, this duality makes it as hard as CNF-SAT: no $O^*((2-epsilon)^n)$ algorithm is known (SETH), and we register $O^*(2^n)$. + 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. - 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 halves $L$ and $R$. For each $x_L in {0,1}^(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^(m slash 2))$ time. 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. + 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$. diff --git a/examples/complexity_consistency_audit.rs b/examples/complexity_consistency_audit.rs index 7387b290e..988bb890f 100644 --- a/examples/complexity_consistency_audit.rs +++ b/examples/complexity_consistency_audit.rs @@ -2,13 +2,13 @@ //! //! For every simple path A -> ... -> B of 1-3 witness hops, substitute the //! path's composed parameter transform into B's registered complexity. The -//! result is an upper bound on solving A (plus the polynomial reduction cost). -//! When that derived bound is strictly smaller in Big-O than A's registered -//! complexity, either A's entry is stale or a transform along the path is -//! wrong; the audit reports the shortest such witness for each variant. -//! -//! The reduction's own running time is not modeled, so a finding whose -//! registered bound is polynomial is only suggestive. +//! 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; @@ -72,9 +72,9 @@ fn extend(graph: &ReductionGraph, path: &mut Vec, found: &mut Vec Option { let composed = graph.compose_path_parameter_transform(path).ok()??; let replacements: HashMap<&str, &Expr> = composed.expressions().collect(); @@ -128,13 +128,16 @@ fn main() { }; let derived_growth = Growth::from_expr(&derived); let registered_growth = Growth::from_expr(&Expr::parse(registered)); - if let Some(failures) = derived_growth.failures().or(registered_growth.failures()) { + 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; - let side = if registered_growth.failures().is_some() { - "registered" - } else { - "derived" - }; for failure in failures { let kind = failure.to_string(); let kind = kind.split(':').next().unwrap_or_default(); @@ -166,7 +169,7 @@ fn main() { println!("Complexity consistency audit (paths of 1-{MAX_HOPS} witness hops)"); println!("paths examined: {}", totals.paths); println!(" consistent: {}", totals.consistent); - println!(" derived is better: {}", totals.violations); + println!(" candidate improvements: {}", totals.violations); println!(" incomparable Big-O: {}", totals.incomparable); println!(" unknown growth: {}", totals.unknown_growth); println!(" uncomposable: {}", totals.uncomposable); @@ -176,7 +179,7 @@ fn main() { } println!( - "\n## Registered bound beaten by a derived bound ({} variants)", + "\n## Candidate improvements requiring manual review ({} variants)", findings.len() ); for (source, list) in &findings {