Clique Is W[1]-Complete

Lax496464.WH_D10_CliqueW1Complete · concepts/Lax496464/WH_D10_CliqueW1Complete.lean · lax-496464

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    pp-Clique is W[1]-complete under fpt-reductions [FG06, Theorems 6.1 and 6.35]: it is in W[1] (WHD01CliqueInW1WH_D01_CliqueInW1), and it is W[1]-hard since it is A[1]-hard (WHD06CliqueA1CompleteWH_D06_CliqueA1Complete) and W[1] = A[1] (WHD09W1EqA1WH_D09_W1EqA1).

    A problem is W[1]-hard as soon as Clique, or any other W[1]-hard problem, fpt-reduces to it (WHA3ReductionCalculus.hardoffptReducesWH_A3_ReductionCalculus.hard_of_fptReduces); it is then not fixed-parameter tractable unless W[1]⊆FPT\mathrm{W}[1] \subseteq \mathrm{FPT} (WHB5HierarchyFacts.notmemFPTofhardWH_B5_HierarchyFacts.not_mem_FPT_of_hard).

    Concept map
    15 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitHub

    1import Lax496464.WH_B4_Hierarchies
    2import Lax496464.WH_C1_GraphProblems
    3
    4/-!
    5---
    6title: Clique Is W[1]-Complete
    7type: theorem
    8---
    9pp-Clique is W[1]-complete under fpt-reductions [FG06, Theorems 6.1 and 6.35]: it is in W[1]
    10(`WH_D01_CliqueInW1`), and it is W[1]-hard since it is A[1]-hard (`WH_D06_CliqueA1Complete`) and
    11W[1] = A[1] (`WH_D09_W1EqA1`).
    12
    13A problem is W[1]-hard as soon as Clique, or any other W[1]-hard problem, fpt-reduces to it
    14(`WH_A3_ReductionCalculus.hard_of_fptReduces`); it is then not fixed-parameter tractable unless
    15W[1]⊆FPT\mathrm{W}[1] \subseteq \mathrm{FPT} (`WH_B5_HierarchyFacts.not_mem_FPT_of_hard`).
    16-/
    17
    18namespace Lax496464.WH_D10_CliqueW1Complete
    19
    20open Lax496464.WH_B4_Hierarchies Lax496464.WH_A2_FptReductions Lax496464.WH_C1_GraphProblems
    21
    22/-- **`p-Clique` is W[1]-complete.** -/
    23axiom clique_W1_complete : Complete (W 1) Clique
    24
    25/-- **`p-Clique` is W[1]-hard.** -/
    26axiom clique_W1_hard : Hard (W 1) Clique
    27
    28end Lax496464.WH_D10_CliqueW1Complete
    29
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…