Skip to content

Commit ef31e35

Browse files
committed
Merge remote-tracking branch 'origin/main' into HEAD
2 parents 2cd0d5a + 888d714 commit ef31e35

7 files changed

Lines changed: 219 additions & 6 deletions

File tree

‎docs/paper/reductions.typ‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5729,7 +5729,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
57295729
#problem-def("NonTautology")[
57305730
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).
57315731
][
5732-
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.
5732+
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)$.
57335733

57345734
*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(", ").
57355735

@@ -10992,7 +10992,7 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
1099210992
][
1099310993
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.
1099410994

10995-
The best known algorithms for general instances use information set decoding techniques, achieving $O(2^(0.0494 n))$ where $n$ is the block length.
10995+
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.
1099610996

1099710997
*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$.
1099810998

‎docs/paper/references.bib‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -984,6 +984,15 @@ @inproceedings{aggarwal2015
984984
doi = {10.1109/FOCS.2015.41}
985985
}
986986

987+
@inproceedings{stephensdavidowitz2019seth,
988+
author = {Noah Stephens-Davidowitz and Vinod Vaikuntanathan},
989+
title = {{SETH}-Hardness of Coding Problems},
990+
booktitle = {Proceedings of the 60th Annual Symposium on Foundations of Computer Science (FOCS)},
991+
pages = {287--301},
992+
year = {2019},
993+
doi = {10.1109/FOCS.2019.00027}
994+
}
995+
987996
@inproceedings{razgon2007,
988997
author = {Igor Razgon},
989998
title = {Computing Minimum Directed Feedback Vertex Set in {$O^*(1.9977^n)$}},
Lines changed: 201 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,201 @@
1+
//! Audit registered variant complexities against the reduction graph.
2+
//!
3+
//! For every simple path A -> ... -> B of 1-3 witness hops, substitute the
4+
//! path's composed parameter transform into B's registered complexity. The
5+
//! resulting expression is a candidate bound on solving A. Substitution of
6+
//! upper-bound parameters requires the target complexity to be monotone in those
7+
//! parameters; a known growth form alone does not prove that property.
8+
//! The audit compares represented growth bounds and reports the shortest route
9+
//! for each candidate improvement. Widening can make a registered bound loose,
10+
//! and the reduction's own running time is not modeled. Every finding therefore
11+
//! requires manual verification of monotonicity, tightness, and reduction cost.
12+
//!
13+
//! cargo run --release --example complexity_consistency_audit
14+
use problemreductions::Growth;
15+
use problemreductions::expr::Expr;
16+
use problemreductions::rules::{ReductionGraph, ReductionPath, ReductionStep};
17+
use std::collections::{BTreeMap, HashMap};
18+
19+
const MAX_HOPS: usize = 3;
20+
21+
type Node = (String, BTreeMap<String, String>);
22+
23+
struct Finding {
24+
path: ReductionPath,
25+
registered: String,
26+
derived: String,
27+
target_complexity: String,
28+
}
29+
30+
#[derive(Default)]
31+
struct Totals {
32+
paths: usize,
33+
no_complexity: usize,
34+
uncomposable: usize,
35+
unknown_growth: usize,
36+
incomparable: usize,
37+
consistent: usize,
38+
violations: usize,
39+
unknown_reasons: BTreeMap<String, usize>,
40+
}
41+
42+
fn extend(graph: &ReductionGraph, path: &mut Vec<Node>, found: &mut Vec<ReductionPath>) {
43+
if path.len() > MAX_HOPS {
44+
return;
45+
}
46+
let (name, variant) = path.last().expect("non-empty path").clone();
47+
for edge in graph.outgoing_reductions(&name) {
48+
// Aggregate-only edges bound a value, not a witness search.
49+
if edge.source_variant != variant || edge.capabilities.turing || !edge.capabilities.witness
50+
{
51+
continue;
52+
}
53+
let next = (edge.target_name.to_string(), edge.target_variant);
54+
if path.contains(&next) {
55+
continue;
56+
}
57+
path.push(next);
58+
found.push(ReductionPath {
59+
steps: path
60+
.iter()
61+
.map(|(name, variant)| ReductionStep {
62+
name: name.clone(),
63+
variant: variant.clone(),
64+
})
65+
.collect(),
66+
});
67+
extend(graph, path, found);
68+
path.pop();
69+
}
70+
}
71+
72+
/// The target complexity rewritten in source parameters, if every step composes.
73+
///
74+
/// Substituting upper-bound fields is sound only for a complexity that is
75+
/// monotone in the substituted parameters. The caller skips unsupported target
76+
/// growth forms, but support is not a monotonicity proof. Findings must be
77+
/// checked against the target formula and each transform's accuracy.
78+
fn derived_complexity(graph: &ReductionGraph, path: &ReductionPath, target: &str) -> Option<Expr> {
79+
let composed = graph.compose_path_parameter_transform(path).ok()??;
80+
let replacements: HashMap<&str, &Expr> = composed.expressions().collect();
81+
Expr::parse(target).substitute_complete(&replacements).ok()
82+
}
83+
84+
fn label(step: &ReductionStep) -> String {
85+
let variant: Vec<&str> = step.variant.values().map(String::as_str).collect();
86+
if variant.is_empty() {
87+
step.name.clone()
88+
} else {
89+
format!("{}/{}", step.name, variant.join("/"))
90+
}
91+
}
92+
93+
fn main() {
94+
let graph = ReductionGraph::new();
95+
let mut paths = Vec::new();
96+
for name in graph.problem_types() {
97+
for variant in graph.variants_for(name) {
98+
extend(&graph, &mut vec![(name.to_string(), variant)], &mut paths);
99+
}
100+
}
101+
102+
let mut totals = Totals::default();
103+
let mut findings: BTreeMap<String, Vec<Finding>> = BTreeMap::new();
104+
for path in paths {
105+
totals.paths += 1;
106+
let (first, last) = (
107+
&path.steps[0],
108+
path.steps.last().expect("path has a target"),
109+
);
110+
let (Some(registered), Some(target)) = (
111+
graph.variant_complexity(&first.name, &first.variant),
112+
graph.variant_complexity(&last.name, &last.variant),
113+
) else {
114+
totals.no_complexity += 1;
115+
continue;
116+
};
117+
if Growth::from_expr(&Expr::parse(target)).failures().is_some() {
118+
totals.unknown_growth += 1;
119+
*totals
120+
.unknown_reasons
121+
.entry("target complexity unsupported".into())
122+
.or_default() += 1;
123+
continue;
124+
}
125+
let Some(derived) = derived_complexity(&graph, &path, target) else {
126+
totals.uncomposable += 1;
127+
continue;
128+
};
129+
let derived_growth = Growth::from_expr(&derived);
130+
let registered_growth = Growth::from_expr(&Expr::parse(registered));
131+
let failure = derived_growth
132+
.failures()
133+
.map(|failures| ("derived", failures))
134+
.or_else(|| {
135+
registered_growth
136+
.failures()
137+
.map(|failures| ("registered", failures))
138+
});
139+
if let Some((side, failures)) = failure {
140+
totals.unknown_growth += 1;
141+
for failure in failures {
142+
let kind = failure.to_string();
143+
let kind = kind.split(':').next().unwrap_or_default();
144+
*totals
145+
.unknown_reasons
146+
.entry(format!("{side}: {kind}"))
147+
.or_default() += 1;
148+
}
149+
continue;
150+
}
151+
let derived_dominates = derived_growth.dominates(&registered_growth);
152+
let registered_dominates = registered_growth.dominates(&derived_growth);
153+
match (registered_dominates, derived_dominates) {
154+
(true, false) => {
155+
totals.violations += 1;
156+
let derived_big_o = derived_growth.to_big_o();
157+
findings.entry(label(first)).or_default().push(Finding {
158+
path,
159+
registered: registered.to_string(),
160+
derived: derived_big_o,
161+
target_complexity: target.to_string(),
162+
});
163+
}
164+
(false, false) => totals.incomparable += 1,
165+
_ => totals.consistent += 1,
166+
}
167+
}
168+
169+
println!("Complexity consistency audit (paths of 1-{MAX_HOPS} witness hops)");
170+
println!("paths examined: {}", totals.paths);
171+
println!(" consistent: {}", totals.consistent);
172+
println!(" candidate improvements: {}", totals.violations);
173+
println!(" incomparable Big-O: {}", totals.incomparable);
174+
println!(" unknown growth: {}", totals.unknown_growth);
175+
println!(" uncomposable: {}", totals.uncomposable);
176+
println!(" no complexity: {}", totals.no_complexity);
177+
for (reason, count) in &totals.unknown_reasons {
178+
println!(" unknown growth, {reason}: {count}");
179+
}
180+
181+
println!(
182+
"\n## Candidate improvements requiring manual review ({} variants)",
183+
findings.len()
184+
);
185+
for (source, list) in &findings {
186+
let best = list
187+
.iter()
188+
.min_by_key(|f| f.path.steps.len())
189+
.expect("non-empty finding list");
190+
let route: Vec<String> = best.path.steps.iter().map(label).collect();
191+
println!("- {source}");
192+
println!(" registered: {}", best.registered);
193+
println!(
194+
" derived: {} ({} witness paths)",
195+
best.derived,
196+
list.len()
197+
);
198+
println!(" via: {}", route.join(" -> "));
199+
println!(" target: {}", best.target_complexity);
200+
}
201+
}

‎src/models/algebraic/minimum_weight_decoding.rs‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,9 @@ impl crate::solvers::BruteForceProblem for MinimumWeightDecoding {
179179
}
180180

181181
crate::declare_variants! {
182-
default MinimumWeightDecoding => "2^(0.0494 * num_cols)" create MinimumWeightDecodingCreateSpec,
182+
// Information set decoding exponents are average-case over random codes. Worst case:
183+
// meet-in-the-middle over the two column halves of H is exact in 2^(m/2).
184+
default MinimumWeightDecoding => "2^(0.5 * num_cols)" create MinimumWeightDecodingCreateSpec,
183185
}
184186

185187
crate::register_brute_force! {

‎src/models/formula/non_tautology.rs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,8 @@ impl crate::solvers::BruteForceProblem for NonTautology {
179179
}
180180

181181
crate::declare_variants! {
182-
default NonTautology => "1.307^num_vars",
182+
// Unbounded-width DNF is CNF-SAT by De Morgan duality; no O*((2-eps)^n) algorithm is known.
183+
default NonTautology => "2^num_vars",
183184
}
184185

185186
crate::register_brute_force! {

‎src/models/graph/max_cut.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -289,7 +289,7 @@ crate::impl_random_generate!(MaxCut<SimpleGraph, i64>, crate::random::SimpleGrap
289289

290290
crate::declare_variants! {
291291
default MaxCut<SimpleGraph, i64> => "2^(2.372 * num_vertices / 3)" create MaxCutI64CreateSpec random,
292-
MaxCut<SimpleGraph, One> => "2^(0.7907 * num_vertices)" create MaxCutOneCreateSpec,
292+
MaxCut<SimpleGraph, One> => "2^(2.372 * num_vertices / 3)" create MaxCutOneCreateSpec,
293293
}
294294

295295
crate::register_brute_force! {

‎src/unit_tests/models/algebraic/minimum_weight_decoding.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ fn test_minimum_weight_decoding_complexity_metadata() {
154154
.find(|entry| entry.name == "MinimumWeightDecoding")
155155
.expect("MinimumWeightDecoding variant entry should exist");
156156

157-
assert_eq!(entry.complexity, "2^(0.0494 * num_cols)");
157+
assert_eq!(entry.complexity, "2^(0.5 * num_cols)");
158158
}
159159

160160
#[test]

0 commit comments

Comments
 (0)