diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 9797e57af..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. + 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$. 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/examples/complexity_consistency_audit.rs b/examples/complexity_consistency_audit.rs new file mode 100644 index 000000000..988bb890f --- /dev/null +++ b/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); + +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, +} + +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) { + // 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 { + 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> = 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(®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 { + 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 = 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 30d9737c2..e3d9ce83b 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. 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! { diff --git a/src/models/formula/non_tautology.rs b/src/models/formula/non_tautology.rs index 1f70c62a0..7d4d4cbff 100644 --- a/src/models/formula/non_tautology.rs +++ b/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! { 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! { diff --git a/src/unit_tests/models/algebraic/minimum_weight_decoding.rs b/src/unit_tests/models/algebraic/minimum_weight_decoding.rs index dfe540ea6..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.0494 * num_cols)"); + assert_eq!(entry.complexity, "2^(0.5 * num_cols)"); } #[test]