oxilean_std/parameterized_complexity/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::Node;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7
8use super::types::{
9    ColorCodingFPT, CourcelleMSOLChecker, CrownDecomposition, FPTAlgorithm, FPTMethod,
10    IterativeCompressionVC, Kernelization, ParamReduction, TreeDecomp, TreeDecomposition,
11    TreewidthAlgorithm, VertexCoverFPT, WClass,
12};
13
14pub fn app(f: Expr, a: Expr) -> Expr {
15    Expr::App(Node::new(f), Node::new(a))
16}
17pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
18    app(app(f, a), b)
19}
20pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
21    app(app2(f, a, b), c)
22}
23pub fn cst(s: &str) -> Expr {
24    Expr::Const(Name::str(s), vec![])
25}
26pub fn prop() -> Expr {
27    Expr::Sort(Level::zero())
28}
29pub fn type0() -> Expr {
30    Expr::Sort(Level::succ(Level::zero()))
31}
32pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
33    Expr::Pi(bi, Name::str(name), Node::new(dom), Node::new(body))
34}
35pub fn arrow(a: Expr, b: Expr) -> Expr {
36    pi(BinderInfo::Default, "_", a, b)
37}
38pub fn bvar(n: u32) -> Expr {
39    Expr::BVar(n)
40}
41pub fn nat_ty() -> Expr {
42    cst("Nat")
43}
44pub fn bool_ty() -> Expr {
45    cst("Bool")
46}
47pub fn real_ty() -> Expr {
48    cst("Real")
49}
50pub fn list_ty(elem: Expr) -> Expr {
51    app(cst("List"), elem)
52}
53pub fn pair_ty(a: Expr, b: Expr) -> Expr {
54    app2(cst("Prod"), a, b)
55}
56pub fn option_ty(a: Expr) -> Expr {
57    app(cst("Option"), a)
58}
59/// `ParameterizedProblem : Type` — a problem with an associated parameter function.
60pub fn parameterized_problem_ty() -> Expr {
61    type0()
62}
63/// `Parameter : Type` — a natural-number parameter extracted from an instance.
64pub fn parameter_ty() -> Expr {
65    arrow(cst("String"), nat_ty())
66}
67/// `FPTAlgorithm : ParameterizedProblem → Type`
68/// An algorithm running in f(k)·n^c time for some computable f and constant c.
69pub fn fpt_algorithm_ty() -> Expr {
70    arrow(parameterized_problem_ty(), type0())
71}
72/// `IsInFPT : ParameterizedProblem → Prop`
73/// The problem is in FPT (Fixed-Parameter Tractable).
74pub fn is_in_fpt_ty() -> Expr {
75    arrow(parameterized_problem_ty(), prop())
76}
77/// `IsInXP : ParameterizedProblem → Prop`
78/// The problem is in XP (solvable in n^f(k) time for each fixed k).
79pub fn is_in_xp_ty() -> Expr {
80    arrow(parameterized_problem_ty(), prop())
81}
82/// `IsWHard : Nat → ParameterizedProblem → Prop`
83/// The problem is W\[i\]-hard (for the given level i of W-hierarchy).
84pub fn is_w_hard_ty() -> Expr {
85    arrow(nat_ty(), arrow(parameterized_problem_ty(), prop()))
86}
87/// `IsWComplete : Nat → ParameterizedProblem → Prop`
88/// The problem is W\[i\]-complete.
89pub fn is_w_complete_ty() -> Expr {
90    arrow(nat_ty(), arrow(parameterized_problem_ty(), prop()))
91}
92/// `FPTReducible : ParameterizedProblem → ParameterizedProblem → Prop`
93/// There exists an FPT-time parameterized reduction between problems.
94pub fn fpt_reducible_ty() -> Expr {
95    arrow(
96        parameterized_problem_ty(),
97        arrow(parameterized_problem_ty(), prop()),
98    )
99}
100/// `WHierarchy : Nat → Type` — the i-th level of the W-hierarchy.
101pub fn w_hierarchy_ty() -> Expr {
102    arrow(nat_ty(), type0())
103}
104/// `W1 : Type` — the class W\[1\] (contains k-clique, k-independent set).
105pub fn w1_ty() -> Expr {
106    type0()
107}
108/// `W2 : Type` — the class W\[2\] (contains k-dominating set, k-set cover).
109pub fn w2_ty() -> Expr {
110    type0()
111}
112/// `WP : Type` — the class W\[P\] (contains weighted circuit satisfiability).
113pub fn wp_ty() -> Expr {
114    type0()
115}
116/// `AW : Type` — the class AW\[*\] (alternating W hierarchy).
117pub fn aw_ty() -> Expr {
118    type0()
119}
120/// `FPT_subset_W1 : FPT ⊆ W\[1\]`
121pub fn fpt_subset_w1_ty() -> Expr {
122    arrow(
123        arrow(parameterized_problem_ty(), cst("IsInFPT")),
124        arrow(parameterized_problem_ty(), app(cst("W1"), bvar(0))),
125    )
126}
127/// `Kernel : ParameterizedProblem → Nat → Type`
128/// A kernelization of size f(k): reduces any instance (x,k) to (x',k') with
129/// |x'| ≤ f(k) and (x,k) ∈ L ↔ (x',k') ∈ L.
130pub fn kernel_ty() -> Expr {
131    arrow(
132        parameterized_problem_ty(),
133        arrow(arrow(nat_ty(), nat_ty()), type0()),
134    )
135}
136/// `HasPolynomialKernel : ParameterizedProblem → Prop`
137/// The problem has a polynomial kernel (|x'| ≤ k^c for some constant c).
138pub fn has_polynomial_kernel_ty() -> Expr {
139    arrow(parameterized_problem_ty(), prop())
140}
141/// `KernelSize : Kernel P f → Nat → Nat`
142/// The size of the kernel as a function of the parameter.
143pub fn kernel_size_ty() -> Expr {
144    arrow(nat_ty(), nat_ty())
145}
146/// `VertexCoverKernel2k : VertexCover has a 2k-vertex kernel`
147pub fn vertex_cover_kernel_2k_ty() -> Expr {
148    prop()
149}
150/// `VertexCoverKernelKSquared : VertexCover has a k^2-vertex kernel (Buss kernel)`
151pub fn vertex_cover_kernel_k_squared_ty() -> Expr {
152    prop()
153}
154/// `TreeDecomposition : Graph → Type`
155/// A tree decomposition: a tree T with bags B_t ⊆ V such that every edge and
156/// vertex is covered, and the bags form connected subtrees.
157pub fn tree_decomposition_ty() -> Expr {
158    arrow(cst("Graph"), type0())
159}
160/// `Treewidth : Graph → Nat`
161/// The treewidth of a graph: min over all tree decompositions of (max bag size − 1).
162pub fn treewidth_ty() -> Expr {
163    arrow(cst("Graph"), nat_ty())
164}
165/// `PathDecomposition : Graph → Type`
166/// A path decomposition: a path (sequence) of bags covering all vertices/edges.
167pub fn path_decomposition_ty() -> Expr {
168    arrow(cst("Graph"), type0())
169}
170/// `Pathwidth : Graph → Nat`
171/// The pathwidth of a graph: min over all path decompositions of (max bag size − 1).
172pub fn pathwidth_ty() -> Expr {
173    arrow(cst("Graph"), nat_ty())
174}
175/// `TreewidthLePathwidth : ∀ G, treewidth G ≤ pathwidth G`
176pub fn treewidth_le_pathwidth_ty() -> Expr {
177    pi(
178        BinderInfo::Default,
179        "G",
180        cst("Graph"),
181        app3(
182            cst("Le"),
183            app(cst("Treewidth"), bvar(0)),
184            app(cst("Pathwidth"), bvar(0)),
185            prop(),
186        ),
187    )
188}
189/// `BranchDecomposition : Graph → Type` — a branch decomposition.
190pub fn branch_decomposition_ty() -> Expr {
191    arrow(cst("Graph"), type0())
192}
193/// `Branchwidth : Graph → Nat`
194pub fn branchwidth_ty() -> Expr {
195    arrow(cst("Graph"), nat_ty())
196}
197/// `FeedbackVertexSet : Graph → Set Vertex → Prop`
198/// S is a FVS if G − S is a forest (acyclic).
199pub fn feedback_vertex_set_ty() -> Expr {
200    arrow(cst("Graph"), arrow(list_ty(nat_ty()), prop()))
201}
202/// `MinFVS : Graph → Nat`
203/// The minimum feedback vertex set size of a graph.
204pub fn min_fvs_ty() -> Expr {
205    arrow(cst("Graph"), nat_ty())
206}
207/// `FVSParameterizedByK : ParameterizedProblem`
208/// The FVS problem parameterized by solution size k — in FPT.
209pub fn fvs_parameterized_ty() -> Expr {
210    parameterized_problem_ty()
211}
212/// `ColorCodingAlgorithm : Nat → Graph → Nat → Bool`
213/// Color-coding for k-path/subgraph: randomly color vertices with k colors
214/// and check for a colorful copy using DP.
215pub fn color_coding_algorithm_ty() -> Expr {
216    arrow(nat_ty(), arrow(cst("Graph"), arrow(nat_ty(), bool_ty())))
217}
218/// `ColorCodingFPT : k-path is in FPT via color coding`
219/// Running time: 2^O(k) · n^O(1).
220pub fn color_coding_fpt_ty() -> Expr {
221    prop()
222}
223/// `PerfectHashFamily : Nat → Nat → Type`
224/// An (n,k)-perfect hash family: a set of functions \[n\]→\[k\] such that
225/// for every k-subset S ⊆ \[n\], some function is injective on S.
226pub fn perfect_hash_family_ty() -> Expr {
227    arrow(nat_ty(), arrow(nat_ty(), type0()))
228}
229/// `MSO2Logic : Type` — Monadic Second-Order Logic (MSO₂) formula.
230pub fn mso2_logic_ty() -> Expr {
231    type0()
232}
233/// `MSO2Satisfies : Graph → MSO2Logic → Prop`
234/// A graph satisfies an MSO₂ formula.
235pub fn mso2_satisfies_ty() -> Expr {
236    arrow(cst("Graph"), arrow(mso2_logic_ty(), prop()))
237}
238/// `CourcelleTheorem : ∀ φ : MSO₂, ∀ k : Nat, CheckMSO2 ∈ FPT(treewidth)`
239/// Every graph property definable in MSO₂ is decidable in linear FPT time
240/// on graphs of bounded treewidth.
241pub fn courcelle_theorem_ty() -> Expr {
242    pi(
243        BinderInfo::Default,
244        "phi",
245        mso2_logic_ty(),
246        pi(BinderInfo::Default, "k", nat_ty(), prop()),
247    )
248}
249/// `BoundedTreewidthDP : Graph → Nat → Prop`
250/// Bounded treewidth dynamic programming: many NP-hard problems are FPT
251/// when parameterized by treewidth.
252pub fn bounded_treewidth_dp_ty() -> Expr {
253    arrow(cst("Graph"), arrow(nat_ty(), prop()))
254}
255/// `ETH : Prop` — Exponential Time Hypothesis
256/// 3-SAT cannot be solved in 2^o(n) time.
257pub fn eth_ty() -> Expr {
258    prop()
259}
260/// `SETH : Prop` — Strong Exponential Time Hypothesis
261/// k-SAT cannot be solved in (2 − ε)^n time for any ε > 0 and all k.
262pub fn seth_ty() -> Expr {
263    prop()
264}
265/// `ETH_implies_no_subexp_fpt : ETH → some problems have no 2^o(k)·poly(n) algorithm`
266pub fn eth_implies_no_subexp_ty() -> Expr {
267    arrow(eth_ty(), prop())
268}
269/// `SETH_implies_no_ons_vc : SETH → VertexCover has no O(1.9999^k) alg unless SETH fails`
270pub fn seth_implies_vc_lb_ty() -> Expr {
271    arrow(seth_ty(), prop())
272}
273/// `SparsificationLemma : 3-SAT with n vars, m clauses reduces to 2^εn instances with O(n) clauses`
274pub fn sparsification_lemma_ty() -> Expr {
275    prop()
276}
277/// `ETH_k_clique_lb : ETH → k-clique needs n^Ω(k) time`
278pub fn eth_k_clique_lb_ty() -> Expr {
279    arrow(eth_ty(), arrow(nat_ty(), prop()))
280}
281/// `FineGrainedReduction : Problem → Problem → Prop`
282/// A fine-grained reduction preserving exact running time exponents.
283pub fn fine_grained_reduction_ty() -> Expr {
284    arrow(
285        parameterized_problem_ty(),
286        arrow(parameterized_problem_ty(), prop()),
287    )
288}
289/// `XPAlgorithm : ParameterizedProblem → Type`
290/// An XP algorithm runs in n^f(k) time for computable f.
291pub fn xp_algorithm_ty() -> Expr {
292    arrow(parameterized_problem_ty(), type0())
293}
294/// `FPT_subset_XP : Every FPT problem is in XP`
295pub fn fpt_subset_xp_ty() -> Expr {
296    pi(
297        BinderInfo::Default,
298        "P",
299        parameterized_problem_ty(),
300        arrow(app(cst("IsInFPT"), bvar(0)), app(cst("IsInXP"), bvar(0))),
301    )
302}
303/// `W1_in_XP : W\[1\] ⊆ XP (assuming W\[1\] ≠ FPT)`
304pub fn w1_in_xp_ty() -> Expr {
305    prop()
306}
307/// `ETHHardness : ParameterizedProblem → Prop`
308/// The problem has no f(k)·2^o(n) algorithm under ETH.
309pub fn eth_hardness_ty() -> Expr {
310    arrow(parameterized_problem_ty(), prop())
311}
312/// `W1Hard_implies_ETH_hard : W\[1\]-hard implies no f(k)·n^g(1) FPT unless W\[1\]=FPT`
313pub fn w1_hard_eth_hard_ty() -> Expr {
314    pi(
315        BinderInfo::Default,
316        "P",
317        parameterized_problem_ty(),
318        arrow(
319            app2(cst("IsWHard"), cst("One"), bvar(0)),
320            arrow(eth_ty(), app(cst("ETHHardness"), bvar(1))),
321        ),
322    )
323}
324/// `kCliqueW1Hard : k-Clique is W\[1\]-complete`
325pub fn k_clique_w1_hard_ty() -> Expr {
326    prop()
327}
328/// `kIndependentSetW1Hard : k-IndependentSet is W\[1\]-complete`
329pub fn k_independent_set_w1_hard_ty() -> Expr {
330    prop()
331}
332/// `kDomSetW2Hard : k-DominatingSet is W\[2\]-complete`
333pub fn k_dom_set_w2_hard_ty() -> Expr {
334    prop()
335}
336/// Build a path decomposition (linear tree decomposition) for a path graph on n vertices.
337/// This gives pathwidth = 1 for a simple path.
338pub fn path_graph_decomp(n: usize) -> TreeDecomp {
339    if n == 0 {
340        return TreeDecomp {
341            bags: vec![],
342            tree_adj: vec![],
343            root: 0,
344        };
345    }
346    let bags: Vec<Vec<usize>> = (0..n.saturating_sub(1)).map(|i| vec![i, i + 1]).collect();
347    let num_bags = bags.len().max(1);
348    let bags = if bags.is_empty() { vec![vec![0]] } else { bags };
349    let mut tree_adj = vec![vec![]; num_bags];
350    for i in 0..num_bags.saturating_sub(1) {
351        tree_adj[i].push(i + 1);
352        tree_adj[i + 1].push(i);
353    }
354    TreeDecomp {
355        bags,
356        tree_adj,
357        root: 0,
358    }
359}
360/// Vertex cover solver using bounded search tree (exponential in k, polynomial in n).
361/// Returns Some(cover) if a vertex cover of size ≤ k exists, else None.
362pub fn vertex_cover_bst(adj: &[Vec<usize>], k: usize) -> Option<Vec<usize>> {
363    fn solve(
364        adj: &[Vec<usize>],
365        cover: &mut Vec<usize>,
366        removed: &mut Vec<bool>,
367        k: usize,
368    ) -> bool {
369        let edge = (0..adj.len()).find_map(|u| {
370            if removed[u] {
371                return None;
372            }
373            adj[u].iter().find(|&&v| !removed[v]).map(|&v| (u, v))
374        });
375        match edge {
376            None => true,
377            Some((u, v)) => {
378                if k == 0 {
379                    return false;
380                }
381                removed[u] = true;
382                cover.push(u);
383                if solve(adj, cover, removed, k - 1) {
384                    removed[u] = false;
385                    return true;
386                }
387                cover.pop();
388                removed[u] = false;
389                removed[v] = true;
390                cover.push(v);
391                if solve(adj, cover, removed, k - 1) {
392                    removed[v] = false;
393                    return true;
394                }
395                cover.pop();
396                removed[v] = false;
397                false
398            }
399        }
400    }
401    let n = adj.len();
402    let mut cover = Vec::new();
403    let mut removed = vec![false; n];
404    if solve(adj, &mut cover, &mut removed, k) {
405        Some(cover)
406    } else {
407        None
408    }
409}
410/// Apply the Crown reduction rule for vertex cover kernelization.
411/// Returns the reduced graph and the vertices already in the cover.
412pub fn crown_reduction(adj: &[Vec<usize>]) -> (Vec<Vec<usize>>, Vec<usize>) {
413    let n = adj.len();
414    let high_deg: Vec<usize> = (0..n).filter(|&v| !adj[v].is_empty()).collect();
415    let mut in_cover = vec![false; n];
416    let mut new_adj: Vec<Vec<usize>> = adj.to_vec();
417    let _ = high_deg;
418    let cover_vertices: Vec<usize> = (0..n).filter(|&v| adj[v].len() > n / 2).collect();
419    for &v in &cover_vertices {
420        in_cover[v] = true;
421        let neighbors = new_adj[v].clone();
422        new_adj[v].clear();
423        for u in neighbors {
424            new_adj[u].retain(|&x| x != v);
425        }
426    }
427    (new_adj, cover_vertices)
428}
429/// Color-coding for k-path detection (simplified randomized version).
430/// Colors vertices randomly with k colors, then checks for a colorful path of length k.
431pub fn color_coding_k_path(adj: &[Vec<usize>], k: usize, seed: u64) -> bool {
432    let n = adj.len();
433    if n == 0 || k == 0 {
434        return k == 0;
435    }
436    if k > n {
437        return false;
438    }
439    let mut rng_state = seed;
440    let next_rand = |state: &mut u64| -> u64 {
441        *state = state
442            .wrapping_mul(6364136223846793005)
443            .wrapping_add(1442695040888963407);
444        *state
445    };
446    let colors: Vec<usize> = (0..n)
447        .map(|_| (next_rand(&mut rng_state) as usize) % k)
448        .collect();
449    let k_capped = k.min(20);
450    let num_subsets = 1usize << k_capped;
451    let mut dp = vec![vec![false; num_subsets]; n];
452    for v in 0..n {
453        let c = colors[v];
454        if c < k_capped {
455            dp[v][1 << c] = true;
456        }
457    }
458    for _len in 1..k_capped {
459        let old_dp = dp.clone();
460        for u in 0..n {
461            for &w in &adj[u] {
462                let cw = colors[w];
463                if cw >= k_capped {
464                    continue;
465                }
466                let cw_bit = 1 << cw;
467                for s in 0..num_subsets {
468                    if old_dp[u][s] && (s & cw_bit == 0) {
469                        dp[w][s | cw_bit] = true;
470                    }
471                }
472            }
473        }
474    }
475    let full_mask = (1 << k_capped) - 1;
476    dp.iter().any(|row| row[full_mask])
477}
478/// Naive treewidth computation for small graphs using elimination ordering.
479/// Returns an upper bound on treewidth via a greedy minimum-degree elimination.
480pub fn treewidth_upper_bound(adj: &[Vec<usize>]) -> usize {
481    let n = adj.len();
482    if n == 0 {
483        return 0;
484    }
485    let mut remaining: Vec<bool> = vec![true; n];
486    let mut adj_copy: Vec<std::collections::HashSet<usize>> = adj
487        .iter()
488        .map(|nbrs| nbrs.iter().cloned().collect())
489        .collect();
490    let mut max_clique = 0usize;
491    for _ in 0..n {
492        let v = (0..n)
493            .filter(|&u| remaining[u])
494            .min_by_key(|&u| adj_copy[u].len())
495            .expect("at least one remaining vertex exists: loop runs n times for n vertices");
496        let deg = adj_copy[v].len();
497        max_clique = max_clique.max(deg);
498        let nbrs: Vec<usize> = adj_copy[v].iter().cloned().collect();
499        for i in 0..nbrs.len() {
500            for j in (i + 1)..nbrs.len() {
501                adj_copy[nbrs[i]].insert(nbrs[j]);
502                adj_copy[nbrs[j]].insert(nbrs[i]);
503            }
504        }
505        remaining[v] = false;
506        for &u in &nbrs {
507            adj_copy[u].remove(&v);
508        }
509        adj_copy[v].clear();
510    }
511    max_clique
512}
513/// Feedback Vertex Set approximation using iterative compression.
514/// Returns an approximate FVS (2-approximation via iterative removal of cycles).
515pub fn fvs_approximation(adj: &[Vec<usize>]) -> Vec<usize> {
516    let n = adj.len();
517    let mut fvs = Vec::new();
518    let mut removed = vec![false; n];
519    loop {
520        let cycle_vertex = find_cycle_vertex(adj, &removed);
521        match cycle_vertex {
522            None => break,
523            Some(v) => {
524                fvs.push(v);
525                removed[v] = true;
526            }
527        }
528    }
529    fvs
530}
531/// Find a vertex on a cycle in the graph (ignoring removed vertices).
532pub fn find_cycle_vertex(adj: &[Vec<usize>], removed: &[bool]) -> Option<usize> {
533    let n = adj.len();
534    let mut color = vec![0u8; n];
535    let mut cycle_v = None;
536    fn dfs(
537        u: usize,
538        parent: usize,
539        adj: &[Vec<usize>],
540        removed: &[bool],
541        color: &mut Vec<u8>,
542        cycle_v: &mut Option<usize>,
543    ) {
544        color[u] = 1;
545        for &v in &adj[u] {
546            if removed[v] || v == parent {
547                continue;
548            }
549            if color[v] == 1 {
550                *cycle_v = Some(v);
551                return;
552            }
553            if color[v] == 0 {
554                dfs(v, u, adj, removed, color, cycle_v);
555                if cycle_v.is_some() {
556                    return;
557                }
558            }
559        }
560        color[u] = 2;
561    }
562    for start in 0..n {
563        if !removed[start] && color[start] == 0 {
564            dfs(start, usize::MAX, adj, removed, &mut color, &mut cycle_v);
565            if cycle_v.is_some() {
566                return cycle_v;
567            }
568        }
569    }
570    None
571}
572/// Check if a given set S is a feedback vertex set for the graph.
573pub fn is_fvs(adj: &[Vec<usize>], fvs: &[usize]) -> bool {
574    let n = adj.len();
575    let mut removed = vec![false; n];
576    for &v in fvs {
577        if v < n {
578            removed[v] = true;
579        }
580    }
581    find_cycle_vertex(adj, &removed).is_none()
582}
583/// Solve k-clique detection by brute force (exponential in k, polynomial baseline).
584/// Used to validate color-coding results.
585pub fn k_clique_brute(adj: &[Vec<usize>], k: usize) -> Option<Vec<usize>> {
586    let n = adj.len();
587    if k == 0 {
588        return Some(vec![]);
589    }
590    if k > n {
591        return None;
592    }
593    fn is_clique(adj: &[Vec<usize>], clique: &[usize]) -> bool {
594        for i in 0..clique.len() {
595            for j in (i + 1)..clique.len() {
596                if !adj[clique[i]].contains(&clique[j]) {
597                    return false;
598                }
599            }
600        }
601        true
602    }
603    fn backtrack(adj: &[Vec<usize>], clique: &mut Vec<usize>, k: usize, start: usize) -> bool {
604        if clique.len() == k {
605            return is_clique(adj, clique);
606        }
607        let n = adj.len();
608        for v in start..n {
609            clique.push(v);
610            if backtrack(adj, clique, k, v + 1) {
611                return true;
612            }
613            clique.pop();
614        }
615        false
616    }
617    let mut clique = Vec::new();
618    if backtrack(adj, &mut clique, k, 0) {
619        Some(clique)
620    } else {
621        None
622    }
623}
624/// Pathwidth computation (exact for trees, upper bound for general graphs).
625pub fn pathwidth_upper_bound(adj: &[Vec<usize>]) -> usize {
626    treewidth_upper_bound(adj)
627}
628/// `CrownDecomposition : Graph → Nat → Prop`
629/// Crown decomposition for vertex cover: a partition V = H ∪ C ∪ R where H is
630/// the head, C is the crown (an independent set matching into H), R is the rest.
631pub fn crown_decomposition_ty() -> Expr {
632    arrow(cst("Graph"), arrow(nat_ty(), prop()))
633}
634/// `CrownReductionRule : Graph → Nat → Graph × Nat`
635/// Given a crown (H, C), remove H and C and reduce k by |H|.
636pub fn crown_reduction_rule_ty() -> Expr {
637    arrow(
638        cst("Graph"),
639        arrow(nat_ty(), pair_ty(cst("Graph"), nat_ty())),
640    )
641}
642/// `LPRelaxationKernel : ParameterizedProblem → Nat → Prop`
643/// LP relaxation half-integrality gives a 2k-vertex kernel for vertex cover.
644pub fn lp_relaxation_kernel_ty() -> Expr {
645    arrow(parameterized_problem_ty(), arrow(nat_ty(), prop()))
646}
647/// `RandomizedKernel : ParameterizedProblem → Nat → Prop`
648/// A randomized kernelization algorithm (correct with high probability).
649pub fn randomized_kernel_ty() -> Expr {
650    arrow(parameterized_problem_ty(), arrow(nat_ty(), prop()))
651}
652/// `KernelComposition : ParameterizedProblem → Prop`
653/// An OR-composition for cross-composition lower bounds on kernelization.
654pub fn kernel_composition_ty() -> Expr {
655    arrow(parameterized_problem_ty(), prop())
656}
657/// `PolynomialKernelLowerBound : ParameterizedProblem → Nat → Prop`
658/// No polynomial kernel of size < k^c unless NP ⊆ coNP/poly.
659pub fn poly_kernel_lower_bound_ty() -> Expr {
660    arrow(parameterized_problem_ty(), arrow(nat_ty(), prop()))
661}
662/// `IterativeCompression : ParameterizedProblem → Prop`
663/// FPT via iterative compression: given a size-(k+1) solution, find a size-k one.
664pub fn iterative_compression_ty() -> Expr {
665    arrow(parameterized_problem_ty(), prop())
666}
667/// `IndependentSetFPT : k-IndependentSet is in FPT via iterative compression (for special graphs)`
668pub fn independent_set_fpt_ty() -> Expr {
669    prop()
670}
671/// `OddCycleTransversalFPT : Odd-Cycle Transversal is FPT via iterative compression`
672pub fn odd_cycle_transversal_fpt_ty() -> Expr {
673    prop()
674}
675/// `CompressionAlgorithm : ParameterizedProblem → Nat → Prop`
676/// Given a (k+1)-solution, the compression algorithm finds a k-solution or returns None.
677pub fn compression_algorithm_ty() -> Expr {
678    arrow(parameterized_problem_ty(), arrow(nat_ty(), prop()))
679}
680/// `UniversalSet : Nat → Nat → Type`
681/// An (n,k)-universal set: a family F of functions \[n\]→{0,1} such that for
682/// every k-subset S ⊆ \[n\], F restricted to S contains all 2^k patterns.
683pub fn universal_set_ty() -> Expr {
684    arrow(nat_ty(), arrow(nat_ty(), type0()))
685}
686/// `UniversalSetSize : Nat → Nat → Nat`
687/// |UniversalSet n k| = O(2^k · k^2 · log n) (Naor-Schulman-Srinivasan).
688pub fn universal_set_size_ty() -> Expr {
689    arrow(nat_ty(), arrow(nat_ty(), nat_ty()))
690}
691/// `DerandomizationViaPHF : k-Subgraph is FPT with deterministic algorithm via PHF`
692pub fn derandomization_via_phf_ty() -> Expr {
693    prop()
694}
695/// `SplittingLemma : Nat → Prop`
696/// The splitting lemma for color-coding: an n-coloring witnesses a colorful copy
697/// with probability ≥ k!/k^k ≥ e^{-k}.
698pub fn splitting_lemma_ty() -> Expr {
699    arrow(nat_ty(), prop())
700}
701/// `MSO1Logic : Type` — Monadic Second-Order Logic MSO₁ (quantifies over vertex sets).
702pub fn mso1_logic_ty() -> Expr {
703    type0()
704}
705/// `MSO1Satisfies : Graph → MSO1Logic → Prop`
706pub fn mso1_satisfies_ty() -> Expr {
707    arrow(cst("Graph"), arrow(mso1_logic_ty(), prop()))
708}
709/// `CourcelleTreewidth : ∀ φ : MSO₂, every bounded-treewidth property is linear-time FPT`
710pub fn courcelle_treewidth_ty() -> Expr {
711    pi(
712        BinderInfo::Default,
713        "phi",
714        mso2_logic_ty(),
715        arrow(nat_ty(), prop()),
716    )
717}
718/// `CourcellePathwidth : MSO₁ model checking is FPT on bounded pathwidth graphs`
719pub fn courcelle_pathwidth_ty() -> Expr {
720    pi(
721        BinderInfo::Default,
722        "phi",
723        mso1_logic_ty(),
724        arrow(nat_ty(), prop()),
725    )
726}
727/// `SeeseSTheorem : MSO₂ model checking is decidable on graphs of bounded clique-width`
728pub fn seese_s_theorem_ty() -> Expr {
729    prop()
730}
731/// `CliqueWidth : Graph → Nat` — the clique-width of a graph.
732pub fn clique_width_ty() -> Expr {
733    arrow(cst("Graph"), nat_ty())
734}
735/// `W1HardnessReduction : Problem → k-Clique` — reduction from k-clique showing W\[1\]-hardness.
736pub fn w1_hardness_reduction_ty() -> Expr {
737    arrow(parameterized_problem_ty(), prop())
738}
739/// `W2HardnessReduction : Problem → k-DominatingSet` — reduction to k-dominating set.
740pub fn w2_hardness_reduction_ty() -> Expr {
741    arrow(parameterized_problem_ty(), prop())
742}
743/// `MulticoloredCliqueW1Hard : Multicolored k-Clique is W\[1\]-complete`
744pub fn multicolored_clique_w1_hard_ty() -> Expr {
745    prop()
746}
747/// `kSetCoverW2Hard : k-SetCover is W\[2\]-complete`
748pub fn k_set_cover_w2_hard_ty() -> Expr {
749    prop()
750}
751/// `kHittingSetW2Hard : k-HittingSet is W\[2\]-complete`
752pub fn k_hitting_set_w2_hard_ty() -> Expr {
753    prop()
754}
755/// `WPHardnessViaCircuit : WP-hardness via weighted circuit satisfiability`
756pub fn wp_hardness_via_circuit_ty() -> Expr {
757    prop()
758}
759/// `GridRamsey : Nat → Nat → Prop`
760/// Grid Ramsey theorem: implications for lower bounds under ETH.
761pub fn grid_ramsey_ty() -> Expr {
762    arrow(nat_ty(), arrow(nat_ty(), prop()))
763}
764/// `ETHKVertexCoverLB : ETH → VertexCover has no 2^o(k) * n algorithm`
765pub fn eth_k_vertex_cover_lb_ty() -> Expr {
766    arrow(eth_ty(), prop())
767}
768/// `ETHKFVSLowerBound : ETH → FVS has no 2^o(k log k) * n algorithm`
769pub fn eth_fvs_lower_bound_ty() -> Expr {
770    arrow(eth_ty(), prop())
771}
772/// `SETHKSATLowerBound : SETH → k-SAT lower bounds for each k`
773pub fn seth_ksat_lower_bound_ty() -> Expr {
774    arrow(seth_ty(), arrow(nat_ty(), prop()))
775}
776/// `ETHImpliesNoSubexpFVS : ETH implies FVS has no f(k)·2^o(sqrt(k)) algorithm`
777pub fn eth_implies_no_subexp_fvs_ty() -> Expr {
778    arrow(eth_ty(), prop())
779}
780/// `SETHImpliesEdgeDominatingSetLB : SETH → Edge Dominating Set has tight lower bounds`
781pub fn seth_edge_dominating_set_lb_ty() -> Expr {
782    arrow(seth_ty(), prop())
783}
784/// `FPTApproximation : ParameterizedProblem → Real → Prop`
785/// An FPT r-approximation runs in f(k)·poly(n) and gives a solution within r of optimal.
786pub fn fpt_approximation_ty() -> Expr {
787    arrow(parameterized_problem_ty(), arrow(real_ty(), prop()))
788}
789/// `GapETH : Prop`
790/// Gap-ETH: there is no FPT approximation scheme for k-Clique unless Gap-ETH fails.
791pub fn gap_eth_ty() -> Expr {
792    prop()
793}
794/// `GapETHImpliesNoFPTAS : Gap-ETH → no FPTAS for k-Clique`
795pub fn gap_eth_no_fptas_ty() -> Expr {
796    arrow(gap_eth_ty(), prop())
797}
798/// `EPTAS : ParameterizedProblem → Prop`
799/// An EPTAS (Efficient PTAS): for each ε > 0, runs in f(1/ε)·poly(n).
800pub fn eptas_ty() -> Expr {
801    arrow(parameterized_problem_ty(), prop())
802}
803/// `PTAS : ParameterizedProblem → Prop`
804/// A PTAS: for each ε > 0, runs in poly(n) (with constant depending on ε).
805pub fn ptas_ty() -> Expr {
806    arrow(parameterized_problem_ty(), prop())
807}
808/// `PlanarEPTAS : Many planar problems have EPTASes via bidimensionality`
809pub fn planar_eptas_ty() -> Expr {
810    prop()
811}
812/// `DualParameter : ParameterizedProblem → Nat → Prop`
813/// Dual parameterization: parameter = n - k (e.g., n - vertex cover size).
814pub fn dual_parameter_ty() -> Expr {
815    arrow(parameterized_problem_ty(), arrow(nat_ty(), prop()))
816}
817/// `AboveGuaranteeParam : ParameterizedProblem → Nat → Prop`
818/// Above-guarantee parameterization: k is the excess above a structural lower bound.
819pub fn above_guarantee_param_ty() -> Expr {
820    arrow(parameterized_problem_ty(), arrow(nat_ty(), prop()))
821}
822/// `StructuralParam : ParameterizedProblem → Type → Prop`
823/// Structural parameterization by a graph parameter (e.g., treewidth, clique-width).
824pub fn structural_param_ty() -> Expr {
825    arrow(parameterized_problem_ty(), arrow(type0(), prop()))
826}
827/// `MaxSATAboveGuarantee : Max-SAT is FPT above the n/2 guarantee`
828pub fn maxsat_above_guarantee_ty() -> Expr {
829    prop()
830}
831/// `VertexCoverAboveMMMatching : VertexCover FPT above max-matching lower bound`
832pub fn vc_above_matching_ty() -> Expr {
833    prop()
834}
835/// `CombinedParameter : ParameterizedProblem → Nat → Nat → Prop`
836/// Combined parameterization: parameterize by both k and a structural parameter.
837pub fn combined_parameter_ty() -> Expr {
838    arrow(
839        parameterized_problem_ty(),
840        arrow(nat_ty(), arrow(nat_ty(), prop())),
841    )
842}
843/// `CountingFPT : ParameterizedProblem → Prop`
844/// The counting version of an FPT problem (count solutions) is also FPT.
845pub fn counting_fpt_ty() -> Expr {
846    arrow(parameterized_problem_ty(), prop())
847}
848/// `SharpW1 : Type` — the class #W\[1\] (parameterized counting analogue of W\[1\]).
849pub fn sharp_w1_ty() -> Expr {
850    type0()
851}
852/// `SharpW2 : Type` — the class #W\[2\].
853pub fn sharp_w2_ty() -> Expr {
854    type0()
855}
856/// `CountingCliquesSharpW1Hard : counting k-cliques is #W\[1\]-complete`
857pub fn counting_cliques_sharp_w1_hard_ty() -> Expr {
858    prop()
859}
860/// `CountingMatchingsSharpW1Hard : counting perfect matchings is #W\[1\]-hard`
861pub fn counting_matchings_sharp_w1_hard_ty() -> Expr {
862    prop()
863}
864/// `CountingHomomorphismsSharpW1 : counting graph homomorphisms is #W\[1\]-complete`
865pub fn counting_homomorphisms_sharp_w1_ty() -> Expr {
866    prop()
867}
868/// `CountingOnBoundedTW : counting on bounded-treewidth graphs is FPT`
869pub fn counting_on_bounded_tw_ty() -> Expr {
870    prop()
871}
872/// `CrownReductionAxiom : Crown decomposition implies 2k-vertex kernel for VC`
873pub fn crown_reduction_axiom_ty() -> Expr {
874    prop()
875}
876/// `KoenigTheoremKernelization : König's theorem gives LP-based kernel`
877pub fn koenig_kernel_ty() -> Expr {
878    prop()
879}
880/// `NemhauserTrotterThm : Nemhauser-Trotter theorem for vertex cover LP kernel`
881pub fn nemhauser_trotter_ty() -> Expr {
882    prop()
883}
884/// `AboveGuaranteeParamVC : VC above matching is FPT (Razgon-O'Sullivan, Cygan et al.)`
885pub fn above_guarantee_vc_ty() -> Expr {
886    prop()
887}
888/// `MaxSNPHardnessInFPT : Max-SNP hard problems have EPTASes in FPT setting`
889pub fn max_snp_fpt_ty() -> Expr {
890    prop()
891}
892/// `MultiparamFPT : FPT algorithms using multiple parameters simultaneously`
893pub fn multiparam_fpt_ty() -> Expr {
894    arrow(nat_ty(), arrow(nat_ty(), prop()))
895}
896/// Alias for `build_parameterized_complexity_env` — simple entry point.
897pub fn build_env(env: &mut Environment) -> Result<(), String> {
898    build_parameterized_complexity_env(env)
899}
900/// Populate an `Environment` with parameterized complexity axioms.
901pub fn build_parameterized_complexity_env(env: &mut Environment) -> Result<(), String> {
902    for (name, ty) in [
903        ("ParameterizedProblem", parameterized_problem_ty()),
904        ("Parameter", parameter_ty()),
905        ("FPTAlgorithm", fpt_algorithm_ty()),
906        ("IsInFPT", is_in_fpt_ty()),
907        ("IsInXP", is_in_xp_ty()),
908        ("IsWHard", is_w_hard_ty()),
909        ("IsWComplete", is_w_complete_ty()),
910        ("FPTReducible", fpt_reducible_ty()),
911        ("WHierarchy", w_hierarchy_ty()),
912        ("W1", w1_ty()),
913        ("W2", w2_ty()),
914        ("WP", wp_ty()),
915        ("AW", aw_ty()),
916        ("Kernel", kernel_ty()),
917        ("HasPolynomialKernel", has_polynomial_kernel_ty()),
918        ("KernelSize", kernel_size_ty()),
919        ("TreeDecomposition", tree_decomposition_ty()),
920        ("Treewidth", treewidth_ty()),
921        ("PathDecomposition", path_decomposition_ty()),
922        ("Pathwidth", pathwidth_ty()),
923        ("BranchDecomposition", branch_decomposition_ty()),
924        ("Branchwidth", branchwidth_ty()),
925        ("FeedbackVertexSet", feedback_vertex_set_ty()),
926        ("MinFVS", min_fvs_ty()),
927        ("ColorCodingAlgorithm", color_coding_algorithm_ty()),
928        ("PerfectHashFamily", perfect_hash_family_ty()),
929        ("MSO2Logic", mso2_logic_ty()),
930        ("MSO2Satisfies", mso2_satisfies_ty()),
931        ("BoundedTreewidthDP", bounded_treewidth_dp_ty()),
932        ("ETH", eth_ty()),
933        ("SETH", seth_ty()),
934        ("ETHHardness", eth_hardness_ty()),
935        ("FineGrainedReduction", fine_grained_reduction_ty()),
936        ("XPAlgorithm", xp_algorithm_ty()),
937        ("kClique", parameterized_problem_ty()),
938        ("kIndependentSet", parameterized_problem_ty()),
939        ("kVertexCover", parameterized_problem_ty()),
940        ("kDominatingSet", parameterized_problem_ty()),
941        ("kFeedbackVertexSet", parameterized_problem_ty()),
942        ("kLongestPath", parameterized_problem_ty()),
943        ("kPathWidth", parameterized_problem_ty()),
944        ("kTreewidth", parameterized_problem_ty()),
945    ] {
946        env.add(Declaration::Axiom {
947            name: Name::str(name),
948            univ_params: vec![],
949            ty,
950        })
951        .ok();
952    }
953    for (name, ty) in [
954        ("ParamComplexity.fpt_subset_xp", fpt_subset_xp_ty()),
955        ("ParamComplexity.k_clique_w1_hard", k_clique_w1_hard_ty()),
956        (
957            "ParamComplexity.k_independent_set_w1_hard",
958            k_independent_set_w1_hard_ty(),
959        ),
960        ("ParamComplexity.k_dom_set_w2_hard", k_dom_set_w2_hard_ty()),
961        (
962            "ParamComplexity.vertex_cover_kernel_2k",
963            vertex_cover_kernel_2k_ty(),
964        ),
965        (
966            "ParamComplexity.vertex_cover_kernel_k_squared",
967            vertex_cover_kernel_k_squared_ty(),
968        ),
969        ("ParamComplexity.color_coding_fpt", color_coding_fpt_ty()),
970        ("ParamComplexity.courcelle_theorem", courcelle_theorem_ty()),
971        (
972            "ParamComplexity.eth_implies_no_subexp",
973            eth_implies_no_subexp_ty(),
974        ),
975        (
976            "ParamComplexity.seth_implies_vc_lb",
977            seth_implies_vc_lb_ty(),
978        ),
979        (
980            "ParamComplexity.sparsification_lemma",
981            sparsification_lemma_ty(),
982        ),
983        ("ParamComplexity.eth_k_clique_lb", eth_k_clique_lb_ty()),
984        ("ParamComplexity.w1_hard_eth_hard", w1_hard_eth_hard_ty()),
985        (
986            "ParamComplexity.treewidth_le_pathwidth",
987            treewidth_le_pathwidth_ty(),
988        ),
989        ("ParamComplexity.fvs_in_fpt", is_in_fpt_ty()),
990        ("ParamComplexity.w1_in_xp", w1_in_xp_ty()),
991        (
992            "ParamComplexity.crown_reduction_axiom",
993            crown_reduction_axiom_ty(),
994        ),
995        ("ParamComplexity.koenig_kernel", koenig_kernel_ty()),
996        ("ParamComplexity.nemhauser_trotter", nemhauser_trotter_ty()),
997        (
998            "ParamComplexity.above_guarantee_vc",
999            above_guarantee_vc_ty(),
1000        ),
1001        (
1002            "ParamComplexity.iterative_compression",
1003            iterative_compression_ty(),
1004        ),
1005        (
1006            "ParamComplexity.independent_set_fpt",
1007            independent_set_fpt_ty(),
1008        ),
1009        (
1010            "ParamComplexity.odd_cycle_transversal_fpt",
1011            odd_cycle_transversal_fpt_ty(),
1012        ),
1013        (
1014            "ParamComplexity.derandomization_via_phf",
1015            derandomization_via_phf_ty(),
1016        ),
1017        (
1018            "ParamComplexity.courcelle_treewidth",
1019            courcelle_treewidth_ty(),
1020        ),
1021        (
1022            "ParamComplexity.courcelle_pathwidth",
1023            courcelle_pathwidth_ty(),
1024        ),
1025        ("ParamComplexity.seese_s_theorem", seese_s_theorem_ty()),
1026        (
1027            "ParamComplexity.multicolored_clique_w1_hard",
1028            multicolored_clique_w1_hard_ty(),
1029        ),
1030        (
1031            "ParamComplexity.k_set_cover_w2_hard",
1032            k_set_cover_w2_hard_ty(),
1033        ),
1034        (
1035            "ParamComplexity.k_hitting_set_w2_hard",
1036            k_hitting_set_w2_hard_ty(),
1037        ),
1038        (
1039            "ParamComplexity.wp_hardness_via_circuit",
1040            wp_hardness_via_circuit_ty(),
1041        ),
1042        (
1043            "ParamComplexity.eth_k_vertex_cover_lb",
1044            eth_k_vertex_cover_lb_ty(),
1045        ),
1046        (
1047            "ParamComplexity.eth_fvs_lower_bound",
1048            eth_fvs_lower_bound_ty(),
1049        ),
1050        ("ParamComplexity.gap_eth", gap_eth_ty()),
1051        ("ParamComplexity.gap_eth_no_fptas", gap_eth_no_fptas_ty()),
1052        (
1053            "ParamComplexity.maxsat_above_guarantee",
1054            maxsat_above_guarantee_ty(),
1055        ),
1056        ("ParamComplexity.vc_above_matching", vc_above_matching_ty()),
1057        (
1058            "ParamComplexity.counting_cliques_sharp_w1_hard",
1059            counting_cliques_sharp_w1_hard_ty(),
1060        ),
1061        (
1062            "ParamComplexity.counting_matchings_sharp_w1_hard",
1063            counting_matchings_sharp_w1_hard_ty(),
1064        ),
1065        (
1066            "ParamComplexity.counting_homomorphisms_sharp_w1",
1067            counting_homomorphisms_sharp_w1_ty(),
1068        ),
1069        (
1070            "ParamComplexity.counting_on_bounded_tw",
1071            counting_on_bounded_tw_ty(),
1072        ),
1073        ("ParamComplexity.planar_eptas", planar_eptas_ty()),
1074        ("ParamComplexity.max_snp_fpt", max_snp_fpt_ty()),
1075    ] {
1076        env.add(Declaration::Axiom {
1077            name: Name::str(name),
1078            univ_params: vec![],
1079            ty,
1080        })
1081        .ok();
1082    }
1083    for (name, ty) in [
1084        ("CrownDecomposition", crown_decomposition_ty()),
1085        ("CrownReductionRule", crown_reduction_rule_ty()),
1086        ("LPRelaxationKernel", lp_relaxation_kernel_ty()),
1087        ("RandomizedKernel", randomized_kernel_ty()),
1088        ("KernelComposition", kernel_composition_ty()),
1089        ("IterativeCompression", iterative_compression_ty()),
1090        ("CompressionAlgorithm", compression_algorithm_ty()),
1091        ("UniversalSet", universal_set_ty()),
1092        ("UniversalSetSize", universal_set_size_ty()),
1093        ("SplittingLemma", splitting_lemma_ty()),
1094        ("MSO1Logic", mso1_logic_ty()),
1095        ("MSO1Satisfies", mso1_satisfies_ty()),
1096        ("CliqueWidth", clique_width_ty()),
1097        ("W1HardnessReduction", w1_hardness_reduction_ty()),
1098        ("W2HardnessReduction", w2_hardness_reduction_ty()),
1099        ("GridRamsey", grid_ramsey_ty()),
1100        ("ETHKVertexCoverLB", eth_k_vertex_cover_lb_ty()),
1101        ("ETHKFVSLowerBound", eth_fvs_lower_bound_ty()),
1102        ("SETHKSATLowerBound", seth_ksat_lower_bound_ty()),
1103        ("FPTApproximation", fpt_approximation_ty()),
1104        ("GapETH", gap_eth_ty()),
1105        ("EPTAS", eptas_ty()),
1106        ("PTAS", ptas_ty()),
1107        ("DualParameter", dual_parameter_ty()),
1108        ("AboveGuaranteeParam", above_guarantee_param_ty()),
1109        ("StructuralParam", structural_param_ty()),
1110        ("CombinedParameter", combined_parameter_ty()),
1111        ("CountingFPT", counting_fpt_ty()),
1112        ("SharpW1", sharp_w1_ty()),
1113        ("SharpW2", sharp_w2_ty()),
1114        ("PolyKernelLowerBound", poly_kernel_lower_bound_ty()),
1115        ("MultiparamFPT", multiparam_fpt_ty()),
1116    ] {
1117        env.add(Declaration::Axiom {
1118            name: Name::str(name),
1119            univ_params: vec![],
1120            ty,
1121        })
1122        .ok();
1123    }
1124    Ok(())
1125}
1126#[cfg(test)]
1127mod tests {
1128    use super::*;
1129    #[test]
1130    fn test_vertex_cover_bst_small() {
1131        let adj = vec![vec![1, 2], vec![0, 2], vec![0, 1]];
1132        let result = vertex_cover_bst(&adj, 2);
1133        assert!(result.is_some(), "Triangle should have 2-vertex cover");
1134        let cover = result.expect("result should be valid");
1135        assert!(cover.len() <= 2);
1136        for u in 0..adj.len() {
1137            for &v in &adj[u] {
1138                assert!(
1139                    cover.contains(&u) || cover.contains(&v),
1140                    "Edge ({}, {}) not covered",
1141                    u,
1142                    v
1143                );
1144            }
1145        }
1146    }
1147    #[test]
1148    fn test_vertex_cover_bst_impossible() {
1149        let adj = vec![vec![1, 2, 3], vec![0, 2, 3], vec![0, 1, 3], vec![0, 1, 2]];
1150        assert!(vertex_cover_bst(&adj, 1).is_none());
1151        assert!(vertex_cover_bst(&adj, 3).is_some());
1152    }
1153    #[test]
1154    fn test_treewidth_upper_bound_path() {
1155        let adj = vec![vec![1], vec![0, 2], vec![1, 3], vec![2, 4], vec![3]];
1156        let tw = treewidth_upper_bound(&adj);
1157        assert!(tw <= 2, "Path should have treewidth ≤ 2, got {}", tw);
1158    }
1159    #[test]
1160    fn test_treewidth_upper_bound_complete() {
1161        let adj = vec![vec![1, 2, 3], vec![0, 2, 3], vec![0, 1, 3], vec![0, 1, 2]];
1162        let tw = treewidth_upper_bound(&adj);
1163        assert!(tw >= 3, "K_4 should have treewidth ≥ 3, got {}", tw);
1164    }
1165    #[test]
1166    fn test_color_coding_k_path() {
1167        let adj = vec![
1168            vec![1],
1169            vec![0, 2],
1170            vec![1, 3],
1171            vec![2, 4],
1172            vec![3, 5],
1173            vec![4],
1174        ];
1175        let found = color_coding_k_path(&adj, 4, 42);
1176        assert!(found, "Should find a 4-path in a 6-path graph");
1177    }
1178    #[test]
1179    fn test_fvs_approximation() {
1180        let adj = vec![vec![1, 3], vec![0, 2], vec![1, 3], vec![2, 0]];
1181        let fvs = fvs_approximation(&adj);
1182        assert!(
1183            is_fvs(&adj, &fvs),
1184            "FVS approximation should produce a valid FVS"
1185        );
1186    }
1187    #[test]
1188    fn test_is_fvs() {
1189        let adj = vec![vec![1, 2], vec![0, 3], vec![0], vec![1]];
1190        assert!(is_fvs(&adj, &[]), "Tree should have empty FVS");
1191        let cycle = vec![vec![1, 3], vec![0, 2], vec![1, 3], vec![2, 0]];
1192        assert!(
1193            is_fvs(&cycle, &[0]),
1194            "Removing vertex 0 from C4 should break all cycles"
1195        );
1196    }
1197    #[test]
1198    fn test_k_clique_brute() {
1199        let adj = vec![vec![1, 2, 3], vec![0, 2, 3], vec![0, 1, 3], vec![0, 1, 2]];
1200        assert!(k_clique_brute(&adj, 3).is_some());
1201        assert!(k_clique_brute(&adj, 5).is_none());
1202    }
1203    #[test]
1204    fn test_build_parameterized_complexity_env() {
1205        let mut env = Environment::new();
1206        let result = build_parameterized_complexity_env(&mut env);
1207        assert!(result.is_ok(), "build should succeed");
1208        assert!(env.get(&Name::str("IsInFPT")).is_some());
1209        assert!(env.get(&Name::str("Treewidth")).is_some());
1210        assert!(env.get(&Name::str("ETH")).is_some());
1211        assert!(env.get(&Name::str("SETH")).is_some());
1212    }
1213    #[test]
1214    fn test_crown_decomposition_tree() {
1215        let adj = vec![vec![1, 2], vec![0, 3], vec![0], vec![1]];
1216        let cd = CrownDecomposition::compute(&adj, 2);
1217        assert!(cd.verify(&adj));
1218    }
1219    #[test]
1220    fn test_crown_decomposition_isolated() {
1221        let adj: Vec<Vec<usize>> = vec![vec![], vec![2], vec![1], vec![]];
1222        let cd = CrownDecomposition::compute(&adj, 1);
1223        assert!(cd.verify(&adj));
1224        assert!(cd.crown.contains(&0) || cd.crown.contains(&3));
1225    }
1226    #[test]
1227    fn test_crown_decomposition_head_size() {
1228        let adj: Vec<Vec<usize>> = vec![vec![], vec![2], vec![1]];
1229        let cd = CrownDecomposition::compute(&adj, 1);
1230        let _ = cd.head_size();
1231    }
1232    #[test]
1233    fn test_color_coding_fpt_construction() {
1234        let cc = ColorCodingFPT::new(4, false);
1235        assert_eq!(cc.k, 4);
1236        assert!(!cc.use_perfect_hash);
1237        assert!(cc.repetitions > 0);
1238        let rt = cc.running_time();
1239        assert!(rt.contains("4"));
1240    }
1241    #[test]
1242    fn test_color_coding_fpt_find_path() {
1243        let adj = vec![
1244            vec![1],
1245            vec![0, 2],
1246            vec![1, 3],
1247            vec![2, 4],
1248            vec![3, 5],
1249            vec![4],
1250        ];
1251        let cc = ColorCodingFPT::new(4, false);
1252        let found = cc.find_k_path(&adj);
1253        assert!(found, "Should find 4-path in 6-path graph");
1254    }
1255    #[test]
1256    fn test_color_coding_fpt_hamiltonian() {
1257        let cc = ColorCodingFPT::new(5, true);
1258        assert!(cc.can_detect_hamiltonian_path(4));
1259        assert!(!cc.can_detect_hamiltonian_path(6));
1260    }
1261    #[test]
1262    fn test_color_coding_fpt_deterministic() {
1263        let cc = ColorCodingFPT::new(3, true);
1264        assert!(cc.use_perfect_hash);
1265        assert_eq!(cc.repetitions, 1);
1266        let rt = cc.running_time();
1267        assert!(rt.contains("deterministic"));
1268    }
1269    #[test]
1270    fn test_courcelle_msol_checker_construction() {
1271        let checker = CourcelleMSOLChecker::new(3, "∃S ⊆ V : |S| ≤ k ∧ S is dominating", 2);
1272        assert_eq!(checker.max_treewidth, 3);
1273        assert_eq!(checker.mso_version, 2);
1274        let rt = checker.running_time();
1275        assert!(rt.contains("treewidth"));
1276    }
1277    #[test]
1278    fn test_courcelle_msol_checker_on_path() {
1279        let adj = vec![vec![1], vec![0, 2], vec![1, 3], vec![2]];
1280        let checker = CourcelleMSOLChecker::new(2, "k-coloring", 1);
1281        assert!(checker.check(&adj));
1282    }
1283    #[test]
1284    fn test_courcelle_msol_checker_on_k4() {
1285        let adj = vec![vec![1, 2, 3], vec![0, 2, 3], vec![0, 1, 3], vec![0, 1, 2]];
1286        let checker_small = CourcelleMSOLChecker::new(2, "3-coloring", 2);
1287        assert!(!checker_small.check(&adj));
1288        let checker_large = CourcelleMSOLChecker::new(5, "3-coloring", 2);
1289        assert!(checker_large.check(&adj));
1290    }
1291    #[test]
1292    fn test_courcelle_decidable_properties() {
1293        let checker = CourcelleMSOLChecker::new(4, "Hamiltonicity", 2);
1294        let desc = checker.decidable_properties();
1295        assert!(desc.contains("treewidth"));
1296    }
1297    #[test]
1298    fn test_vertex_cover_fpt_solve_triangle() {
1299        let adj = vec![vec![1, 2], vec![0, 2], vec![0, 1]];
1300        let vc = VertexCoverFPT::new(2);
1301        let result = vc.solve(&adj);
1302        assert!(result.is_some(), "Triangle has a 2-vertex cover");
1303        let cover = result.expect("result should be valid");
1304        for u in 0..adj.len() {
1305            for &v in &adj[u] {
1306                assert!(cover.contains(&u) || cover.contains(&v));
1307            }
1308        }
1309    }
1310    #[test]
1311    fn test_vertex_cover_fpt_solve_k4() {
1312        let adj = vec![vec![1, 2, 3], vec![0, 2, 3], vec![0, 1, 3], vec![0, 1, 2]];
1313        let vc3 = VertexCoverFPT::new(3);
1314        assert!(vc3.solve(&adj).is_some());
1315        let vc1 = VertexCoverFPT::new(1);
1316        assert!(vc1.solve(&adj).is_none());
1317    }
1318    #[test]
1319    fn test_vertex_cover_fpt_running_time() {
1320        let vc = VertexCoverFPT::new(5);
1321        let rt = vc.running_time();
1322        assert!(rt.contains("5"));
1323    }
1324    #[test]
1325    fn test_vertex_cover_fpt_lp_kernel() {
1326        let adj = vec![vec![1, 2, 3, 4], vec![0], vec![0], vec![0], vec![0]];
1327        let vc = VertexCoverFPT::new(3);
1328        let (_, cover, _) = vc.lp_kernel(&adj);
1329        assert!(cover.contains(&0), "Center should be in LP kernel cover");
1330    }
1331    #[test]
1332    fn test_iterative_compression_vc_triangle() {
1333        let adj = vec![vec![1, 2], vec![0, 2], vec![0, 1]];
1334        let ic = IterativeCompressionVC::new(2);
1335        let over_cover = vec![0, 1, 2];
1336        let result = ic.compress(&adj, &over_cover);
1337        assert!(result.is_some(), "Triangle should compress to 2-cover");
1338    }
1339    #[test]
1340    fn test_iterative_compression_vc_impossible() {
1341        let adj = vec![vec![1, 2, 3], vec![0, 2, 3], vec![0, 1, 3], vec![0, 1, 2]];
1342        let ic = IterativeCompressionVC::new(1);
1343        let over_cover = vec![0, 1];
1344        let result = ic.compress(&adj, &over_cover);
1345        assert!(result.is_none(), "K_4 cannot be covered by 1 vertex");
1346    }
1347    #[test]
1348    fn test_build_parameterized_complexity_env_new() {
1349        let mut env = Environment::new();
1350        let result = build_parameterized_complexity_env(&mut env);
1351        assert!(result.is_ok());
1352        assert!(env.get(&Name::str("CrownDecomposition")).is_some());
1353        assert!(env.get(&Name::str("SharpW1")).is_some());
1354        assert!(env.get(&Name::str("GapETH")).is_some());
1355        assert!(env.get(&Name::str("EPTAS")).is_some());
1356        assert!(env.get(&Name::str("MSO1Logic")).is_some());
1357        assert!(env.get(&Name::str("CliqueWidth")).is_some());
1358        assert!(env.get(&Name::str("UniversalSet")).is_some());
1359        assert!(env.get(&Name::str("DualParameter")).is_some());
1360    }
1361}
1362#[cfg(test)]
1363mod tests_pc_extra {
1364    use super::*;
1365    #[test]
1366    fn test_fpt_algorithm() {
1367        let bst = FPTMethod::bounded_search_tree_vc();
1368        assert!(bst.is_single_exponential());
1369        let r = bst.runtime(5, 1000);
1370        assert!((r - 32000.0).abs() < 1e-6);
1371    }
1372    #[test]
1373    fn test_kernelization() {
1374        let vc = Kernelization::vertex_cover_2k();
1375        assert!(vc.is_polynomial_kernel());
1376        let sz = vc.kernel_size(10);
1377        assert_eq!(sz, Some(20.0));
1378        let fvs = Kernelization::feedback_vertex_set();
1379        assert!(fvs.is_polynomial_kernel());
1380    }
1381    #[test]
1382    fn test_w_hierarchy() {
1383        let vc = WClass::vertex_cover_class();
1384        assert!(vc.is_fpt());
1385        let cl = WClass::clique_class();
1386        assert!(!cl.is_fpt());
1387        assert!(!cl.harder_than_w1());
1388        let ds = WClass::dominating_set_class();
1389        assert!(ds.harder_than_w1());
1390        assert!(ds > cl);
1391    }
1392    #[test]
1393    fn test_treewidth_algorithm() {
1394        let sat = TreewidthAlgorithm::satisfiability_tw();
1395        assert!(sat.is_linear_time_in_n());
1396        let r = sat.runtime(3, 100);
1397        assert!((r - 800.0).abs() < 1e-6);
1398    }
1399    #[test]
1400    fn test_param_reduction() {
1401        let red = ParamReduction::new("IndependentSet", "Clique", "k", "k", "f(k)=k");
1402        assert!(red.is_fpt_reduction());
1403        let bad_red = ParamReduction::new("A", "B", "k", "k+log(n)", "k+log(n)");
1404        assert!(!bad_red.is_fpt_reduction());
1405    }
1406}
oxilean_std/parameterized_complexity/functions.rs

oxilean_std/parameterized_complexity/
functions.rs
