Polynomial-time many-one reductions and NP-completeness

This file defines polynomial-time many-one (Karp) reductions L ≤ₚ L' and the derived notions NPHard and NPComplete, following Arora–Barak (Definitions 2.7, 2.8).

A reduction L ≤ₚ L' is a polynomial-time computable function f (i.e. f ∈ FP) such that x ∈ L ↔ f x ∈ L'. A language is NP-hard when every language in NP reduces to it, and NP-complete when it is additionally a member of NP.

The headline application is SAT.NPComplete_language (Cook–Levin), in Complexitylib/SAT/CookLevin.lean.

def Complexity.MapReducesPoly (L L' : Language) : Prop

Polynomial-time many-one reduction. MapReducesPoly L L' (written L ≤ₚ L') holds when there is a polynomial-time computable function f (f ∈ FP) with x ∈ L ↔ f x ∈ L' for every input x.

Equations

• (L ≤ₚ L') = ∃ f ∈ Complexity.FP, ∀ (x : List Bool), x ∈ L ↔ f x ∈ L'

def Complexity.«term_≤ₚ_» : Lean.TrailingParserDescr

Polynomial-time many-one reduction. MapReducesPoly L L' (written L ≤ₚ L') holds when there is a polynomial-time computable function f (f ∈ FP) with x ∈ L ↔ f x ∈ L' for every input x.

Equations

• Complexity.«term_≤ₚ_» = Lean.ParserDescr.trailingNode `Complexity.«term_≤ₚ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₚ ") (Lean.ParserDescr.cat `term 51))

def Complexity.NPHard (L : Language) : Prop

NP-hardness. L is NP-hard when every language in NP reduces to L in polynomial time.

Equations

• Complexity.NPHard L = ∀ L' ∈ Complexity.NP, L' ≤ₚ L

def Complexity.NPComplete (L : Language) : Prop

NP-completeness. L is NP-complete when it is in NP and NP-hard.

Equations

• Complexity.NPComplete L = (L ∈ Complexity.NP ∧ Complexity.NPHard L)