Skip to main content

Module functions

oxilean_std::parameterized_complexity

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

above_guarantee_param_ty
AboveGuaranteeParam : ParameterizedProblem β†’ Nat β†’ Prop Above-guarantee parameterization: k is the excess above a structural lower bound.
above_guarantee_vc_ty
AboveGuaranteeParamVC : VC above matching is FPT (Razgon-O'Sullivan, Cygan et al.)
app
app2
app3
arrow
aw_ty
AW : Type β€” the class AW[*] (alternating W hierarchy).
bool_ty
bounded_treewidth_dp_ty
BoundedTreewidthDP : Graph β†’ Nat β†’ Prop Bounded treewidth dynamic programming: many NP-hard problems are FPT when parameterized by treewidth.
branch_decomposition_ty
BranchDecomposition : Graph β†’ Type β€” a branch decomposition.
branchwidth_ty
Branchwidth : Graph β†’ Nat
build_env
Alias for build_parameterized_complexity_env β€” simple entry point.
build_parameterized_complexity_env
Populate an Environment with parameterized complexity axioms.
bvar
clique_width_ty
CliqueWidth : Graph β†’ Nat β€” the clique-width of a graph.
color_coding_algorithm_ty
ColorCodingAlgorithm : Nat β†’ Graph β†’ Nat β†’ Bool Color-coding for k-path/subgraph: randomly color vertices with k colors and check for a colorful copy using DP.
color_coding_fpt_ty
ColorCodingFPT : k-path is in FPT via color coding Running time: 2^O(k) Β· n^O(1).
color_coding_k_path
Color-coding for k-path detection (simplified randomized version). Colors vertices randomly with k colors, then checks for a colorful path of length k.
combined_parameter_ty
CombinedParameter : ParameterizedProblem β†’ Nat β†’ Nat β†’ Prop Combined parameterization: parameterize by both k and a structural parameter.
compression_algorithm_ty
CompressionAlgorithm : ParameterizedProblem β†’ Nat β†’ Prop Given a (k+1)-solution, the compression algorithm finds a k-solution or returns None.
counting_cliques_sharp_w1_hard_ty
CountingCliquesSharpW1Hard : counting k-cliques is #W[1]-complete
counting_fpt_ty
CountingFPT : ParameterizedProblem β†’ Prop The counting version of an FPT problem (count solutions) is also FPT.
counting_homomorphisms_sharp_w1_ty
CountingHomomorphismsSharpW1 : counting graph homomorphisms is #W[1]-complete
counting_matchings_sharp_w1_hard_ty
CountingMatchingsSharpW1Hard : counting perfect matchings is #W[1]-hard
counting_on_bounded_tw_ty
CountingOnBoundedTW : counting on bounded-treewidth graphs is FPT
courcelle_pathwidth_ty
CourcellePathwidth : MSO₁ model checking is FPT on bounded pathwidth graphs
courcelle_theorem_ty
CourcelleTheorem : βˆ€ Ο† : MSOβ‚‚, βˆ€ k : Nat, CheckMSO2 ∈ FPT(treewidth) Every graph property definable in MSOβ‚‚ is decidable in linear FPT time on graphs of bounded treewidth.
courcelle_treewidth_ty
CourcelleTreewidth : βˆ€ Ο† : MSOβ‚‚, every bounded-treewidth property is linear-time FPT
crown_decomposition_ty
CrownDecomposition : Graph β†’ Nat β†’ Prop Crown decomposition for vertex cover: a partition V = H βˆͺ C βˆͺ R where H is the head, C is the crown (an independent set matching into H), R is the rest.
crown_reduction
Apply the Crown reduction rule for vertex cover kernelization. Returns the reduced graph and the vertices already in the cover.
crown_reduction_axiom_ty
CrownReductionAxiom : Crown decomposition implies 2k-vertex kernel for VC
crown_reduction_rule_ty
CrownReductionRule : Graph β†’ Nat β†’ Graph Γ— Nat Given a crown (H, C), remove H and C and reduce k by |H|.
cst
derandomization_via_phf_ty
DerandomizationViaPHF : k-Subgraph is FPT with deterministic algorithm via PHF
dual_parameter_ty
DualParameter : ParameterizedProblem β†’ Nat β†’ Prop Dual parameterization: parameter = n - k (e.g., n - vertex cover size).
eptas_ty
EPTAS : ParameterizedProblem β†’ Prop An EPTAS (Efficient PTAS): for each Ξ΅ > 0, runs in f(1/Ξ΅)Β·poly(n).
eth_fvs_lower_bound_ty
ETHKFVSLowerBound : ETH β†’ FVS has no 2^o(k log k) * n algorithm
eth_hardness_ty
ETHHardness : ParameterizedProblem β†’ Prop The problem has no f(k)Β·2^o(n) algorithm under ETH.
eth_implies_no_subexp_fvs_ty
ETHImpliesNoSubexpFVS : ETH implies FVS has no f(k)Β·2^o(sqrt(k)) algorithm
eth_implies_no_subexp_ty
ETH_implies_no_subexp_fpt : ETH β†’ some problems have no 2^o(k)Β·poly(n) algorithm
eth_k_clique_lb_ty
ETH_k_clique_lb : ETH β†’ k-clique needs n^Ξ©(k) time
eth_k_vertex_cover_lb_ty
ETHKVertexCoverLB : ETH β†’ VertexCover has no 2^o(k) * n algorithm
eth_ty
ETH : Prop β€” Exponential Time Hypothesis 3-SAT cannot be solved in 2^o(n) time.
feedback_vertex_set_ty
FeedbackVertexSet : Graph β†’ Set Vertex β†’ Prop S is a FVS if G βˆ’ S is a forest (acyclic).
find_cycle_vertex
Find a vertex on a cycle in the graph (ignoring removed vertices).
fine_grained_reduction_ty
FineGrainedReduction : Problem β†’ Problem β†’ Prop A fine-grained reduction preserving exact running time exponents.
fpt_algorithm_ty
FPTAlgorithm : ParameterizedProblem β†’ Type An algorithm running in f(k)Β·n^c time for some computable f and constant c.
fpt_approximation_ty
FPTApproximation : ParameterizedProblem β†’ Real β†’ Prop An FPT r-approximation runs in f(k)Β·poly(n) and gives a solution within r of optimal.
fpt_reducible_ty
FPTReducible : ParameterizedProblem β†’ ParameterizedProblem β†’ Prop There exists an FPT-time parameterized reduction between problems.
fpt_subset_w1_ty
FPT_subset_W1 : FPT βŠ† W[1]
fpt_subset_xp_ty
FPT_subset_XP : Every FPT problem is in XP
fvs_approximation
Feedback Vertex Set approximation using iterative compression. Returns an approximate FVS (2-approximation via iterative removal of cycles).
fvs_parameterized_ty
FVSParameterizedByK : ParameterizedProblem The FVS problem parameterized by solution size k β€” in FPT.
gap_eth_no_fptas_ty
GapETHImpliesNoFPTAS : Gap-ETH β†’ no FPTAS for k-Clique
gap_eth_ty
GapETH : Prop Gap-ETH: there is no FPT approximation scheme for k-Clique unless Gap-ETH fails.
grid_ramsey_ty
GridRamsey : Nat β†’ Nat β†’ Prop Grid Ramsey theorem: implications for lower bounds under ETH.
has_polynomial_kernel_ty
HasPolynomialKernel : ParameterizedProblem β†’ Prop The problem has a polynomial kernel (|x’| ≀ k^c for some constant c).
independent_set_fpt_ty
IndependentSetFPT : k-IndependentSet is in FPT via iterative compression (for special graphs)
is_fvs
Check if a given set S is a feedback vertex set for the graph.
is_in_fpt_ty
IsInFPT : ParameterizedProblem β†’ Prop The problem is in FPT (Fixed-Parameter Tractable).
is_in_xp_ty
IsInXP : ParameterizedProblem β†’ Prop The problem is in XP (solvable in n^f(k) time for each fixed k).
is_w_complete_ty
IsWComplete : Nat β†’ ParameterizedProblem β†’ Prop The problem is W[i]-complete.
is_w_hard_ty
IsWHard : Nat β†’ ParameterizedProblem β†’ Prop The problem is W[i]-hard (for the given level i of W-hierarchy).
iterative_compression_ty
IterativeCompression : ParameterizedProblem β†’ Prop FPT via iterative compression: given a size-(k+1) solution, find a size-k one.
k_clique_brute
Solve k-clique detection by brute force (exponential in k, polynomial baseline). Used to validate color-coding results.
k_clique_w1_hard_ty
kCliqueW1Hard : k-Clique is W[1]-complete
k_dom_set_w2_hard_ty
kDomSetW2Hard : k-DominatingSet is W[2]-complete
k_hitting_set_w2_hard_ty
kHittingSetW2Hard : k-HittingSet is W[2]-complete
k_independent_set_w1_hard_ty
kIndependentSetW1Hard : k-IndependentSet is W[1]-complete
k_set_cover_w2_hard_ty
kSetCoverW2Hard : k-SetCover is W[2]-complete
kernel_composition_ty
KernelComposition : ParameterizedProblem β†’ Prop An OR-composition for cross-composition lower bounds on kernelization.
kernel_size_ty
KernelSize : Kernel P f β†’ Nat β†’ Nat The size of the kernel as a function of the parameter.
kernel_ty
Kernel : ParameterizedProblem β†’ Nat β†’ Type A kernelization of size f(k): reduces any instance (x,k) to (x’,k’) with |x’| ≀ f(k) and (x,k) ∈ L ↔ (x’,k’) ∈ L.
koenig_kernel_ty
KoenigTheoremKernelization : KΓΆnig's theorem gives LP-based kernel
list_ty
lp_relaxation_kernel_ty
LPRelaxationKernel : ParameterizedProblem β†’ Nat β†’ Prop LP relaxation half-integrality gives a 2k-vertex kernel for vertex cover.
max_snp_fpt_ty
MaxSNPHardnessInFPT : Max-SNP hard problems have EPTASes in FPT setting
maxsat_above_guarantee_ty
MaxSATAboveGuarantee : Max-SAT is FPT above the n/2 guarantee
min_fvs_ty
MinFVS : Graph β†’ Nat The minimum feedback vertex set size of a graph.
mso1_logic_ty
MSO1Logic : Type β€” Monadic Second-Order Logic MSO₁ (quantifies over vertex sets).
mso1_satisfies_ty
MSO1Satisfies : Graph β†’ MSO1Logic β†’ Prop
mso2_logic_ty
MSO2Logic : Type β€” Monadic Second-Order Logic (MSOβ‚‚) formula.
mso2_satisfies_ty
MSO2Satisfies : Graph β†’ MSO2Logic β†’ Prop A graph satisfies an MSOβ‚‚ formula.
multicolored_clique_w1_hard_ty
MulticoloredCliqueW1Hard : Multicolored k-Clique is W[1]-complete
multiparam_fpt_ty
MultiparamFPT : FPT algorithms using multiple parameters simultaneously
nat_ty
nemhauser_trotter_ty
NemhauserTrotterThm : Nemhauser-Trotter theorem for vertex cover LP kernel
odd_cycle_transversal_fpt_ty
OddCycleTransversalFPT : Odd-Cycle Transversal is FPT via iterative compression
option_ty
pair_ty
parameter_ty
Parameter : Type β€” a natural-number parameter extracted from an instance.
parameterized_problem_ty
ParameterizedProblem : Type β€” a problem with an associated parameter function.
path_decomposition_ty
PathDecomposition : Graph β†’ Type A path decomposition: a path (sequence) of bags covering all vertices/edges.
path_graph_decomp
Build a path decomposition (linear tree decomposition) for a path graph on n vertices. This gives pathwidth = 1 for a simple path.
pathwidth_ty
Pathwidth : Graph β†’ Nat The pathwidth of a graph: min over all path decompositions of (max bag size βˆ’ 1).
pathwidth_upper_bound
Pathwidth computation (exact for trees, upper bound for general graphs).
perfect_hash_family_ty
PerfectHashFamily : Nat β†’ Nat β†’ Type An (n,k)-perfect hash family: a set of functions [n]β†’[k] such that for every k-subset S βŠ† [n], some function is injective on S.
pi
planar_eptas_ty
PlanarEPTAS : Many planar problems have EPTASes via bidimensionality
poly_kernel_lower_bound_ty
PolynomialKernelLowerBound : ParameterizedProblem β†’ Nat β†’ Prop No polynomial kernel of size < k^c unless NP βŠ† coNP/poly.
prop
ptas_ty
PTAS : ParameterizedProblem β†’ Prop A PTAS: for each Ξ΅ > 0, runs in poly(n) (with constant depending on Ξ΅).
randomized_kernel_ty
RandomizedKernel : ParameterizedProblem β†’ Nat β†’ Prop A randomized kernelization algorithm (correct with high probability).
real_ty
seese_s_theorem_ty
SeeseSTheorem : MSOβ‚‚ model checking is decidable on graphs of bounded clique-width
seth_edge_dominating_set_lb_ty
SETHImpliesEdgeDominatingSetLB : SETH β†’ Edge Dominating Set has tight lower bounds
seth_implies_vc_lb_ty
SETH_implies_no_ons_vc : SETH β†’ VertexCover has no O(1.9999^k) alg unless SETH fails
seth_ksat_lower_bound_ty
SETHKSATLowerBound : SETH β†’ k-SAT lower bounds for each k
seth_ty
SETH : Prop β€” Strong Exponential Time Hypothesis k-SAT cannot be solved in (2 βˆ’ Ξ΅)^n time for any Ξ΅ > 0 and all k.
sharp_w1_ty
SharpW1 : Type β€” the class #W[1] (parameterized counting analogue of W[1]).
sharp_w2_ty
SharpW2 : Type β€” the class #W[2].
sparsification_lemma_ty
SparsificationLemma : 3-SAT with n vars, m clauses reduces to 2^Ξ΅n instances with O(n) clauses
splitting_lemma_ty
SplittingLemma : Nat β†’ Prop The splitting lemma for color-coding: an n-coloring witnesses a colorful copy with probability β‰₯ k!/k^k β‰₯ e^{-k}.
structural_param_ty
StructuralParam : ParameterizedProblem β†’ Type β†’ Prop Structural parameterization by a graph parameter (e.g., treewidth, clique-width).
tree_decomposition_ty
TreeDecomposition : Graph β†’ Type A tree decomposition: a tree T with bags B_t βŠ† V such that every edge and vertex is covered, and the bags form connected subtrees.
treewidth_le_pathwidth_ty
TreewidthLePathwidth : βˆ€ G, treewidth G ≀ pathwidth G
treewidth_ty
Treewidth : Graph β†’ Nat The treewidth of a graph: min over all tree decompositions of (max bag size βˆ’ 1).
treewidth_upper_bound
Naive treewidth computation for small graphs using elimination ordering. Returns an upper bound on treewidth via a greedy minimum-degree elimination.
type0
universal_set_size_ty
UniversalSetSize : Nat β†’ Nat β†’ Nat |UniversalSet n k| = O(2^k Β· k^2 Β· log n) (Naor-Schulman-Srinivasan).
universal_set_ty
UniversalSet : Nat β†’ Nat β†’ Type An (n,k)-universal set: a family F of functions [n]β†’{0,1} such that for every k-subset S βŠ† [n], F restricted to S contains all 2^k patterns.
vc_above_matching_ty
VertexCoverAboveMMMatching : VertexCover FPT above max-matching lower bound
vertex_cover_bst
Vertex cover solver using bounded search tree (exponential in k, polynomial in n). Returns Some(cover) if a vertex cover of size ≀ k exists, else None.
vertex_cover_kernel_2k_ty
VertexCoverKernel2k : VertexCover has a 2k-vertex kernel
vertex_cover_kernel_k_squared_ty
VertexCoverKernelKSquared : VertexCover has a k^2-vertex kernel (Buss kernel)
w1_hard_eth_hard_ty
W1Hard_implies_ETH_hard : W[1]-hard implies no f(k)Β·n^g(1) FPT unless W[1]=FPT
w1_hardness_reduction_ty
W1HardnessReduction : Problem β†’ k-Clique β€” reduction from k-clique showing W[1]-hardness.
w1_in_xp_ty
W1_in_XP : W[1] βŠ† XP (assuming W[1] β‰  FPT)
w1_ty
W1 : Type β€” the class W[1] (contains k-clique, k-independent set).
w2_hardness_reduction_ty
W2HardnessReduction : Problem β†’ k-DominatingSet β€” reduction to k-dominating set.
w2_ty
W2 : Type β€” the class W[2] (contains k-dominating set, k-set cover).
w_hierarchy_ty
WHierarchy : Nat β†’ Type β€” the i-th level of the W-hierarchy.
wp_hardness_via_circuit_ty
WPHardnessViaCircuit : WP-hardness via weighted circuit satisfiability
wp_ty
WP : Type β€” the class W[P] (contains weighted circuit satisfiability).
xp_algorithm_ty
XPAlgorithm : ParameterizedProblem β†’ Type An XP algorithm runs in n^f(k) time for computable f.