Dave Ishii - Problem Solving Blog

-- We assume a (mostly hypothetical) library for complexity theory
import Computability.NP
-- We use real mathlib tools for graphs, finite sets, and matrices
import Mathlib.Combinatorics.SimpleGraph
import Mathlib.Data.Fintype
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Finset

open Finset SimpleGraph

-- This (hypothetical) library would define:

-- A type for decision problems (languages) over an input type α
class Language (α : Type) where
  P : α → Prop

-- A definition for a problem being in NP
def NP {α} (L : Language α) : Prop := sorry -- (Exists a poly-time verifier)

-- A definition for a problem being NP-hard
def NPHard {α} (L : Language α) : Prop := sorry -- (All NP problems poly-time reduce to L)

-- A problem is NP-complete if it's in NP and is NP-hard
def NPComplete {α} (L : Language α) : Prop :=
  NP L ∧ NPHard L

-- A type for Boolean formulas in 3-Conjunctive Normal Form (3-CNF)
structure ThreeSAT.Formula (v : Type) :=
  clauses : Finset (Fin 3 → Option Bool × v) -- Each clause has 3 literals

-- The 3-SAT decision problem
def ThreeSAT_problem : Language (ThreeSAT.Formula ℕ) :=
  { P := fun φ => ∃ (assign : ℕ → Bool), sorry -- ... formula φ is satisfied by assign
  }

-- The foundational axiom for all subsequent proofs:
axiom ThreeSAT_is_NPComplete : NPComplete ThreeSAT_problem

-- An instance of 0-1 ILP is a matrix A and a vector b over integers
structure ZeroOneILP.Instance :=
  (m n : ℕ)
  (A : Matrix (Fin m) (Fin n) ℤ)
  (b : Fin m → ℤ)

-- The decision problem for 0-1 ILP
def ZeroOneILP_problem : Language ZeroOneILP.Instance :=
  { P := fun inst =>
      -- There exists a vector x of 0s and 1s
      ∃ (x : Fin inst.n → Fin 2),
        -- Such that A * x <= b
        ∀ (i : Fin inst.m),
          (Matrix.dotProduct (inst.A i) (fun j => (x j : ℤ))) ≤ inst.b i
  }

-- Theorem: 0-1 Integer Programming is NP-complete
theorem ZeroOneILP_is_NPComplete : NPComplete ZeroOneILP_problem :=
by
  constructor
  · -- Part 1: Prove ZeroOneILP is in NP
    -- We must show that a given solution x can be verified in polynomial time.
    -- This involves a polynomial-time matrix-vector multiplication and comparison.
    apply (NP_verifier_poly_time :
      NP ZeroOneILP_problem)
    sorry -- This proof is complex, involving formalizing algorithm runtime.
  · -- Part 2: Prove ZeroOneILP is NP-hard
    -- We show this by reducing 3-SAT to it.
    apply (NPHard_of_reduction :
      -- We assume 3-SAT is NP-hard (from our axiom)
      NPHard ThreeSAT_problem →
      -- We provide a polynomial-time reduction from 3-SAT to 0-1 ILP
      (∃ (f : ThreeSAT.Formula ℕ → ZeroOneILP.Instance),
        (PolyTimeReduction f) ∧
        -- And prove the reduction is correct
        (∀ (φ : ThreeSAT.Formula ℕ),
          ThreeSAT_problem.P φ ↔ ZeroOneILP_problem.P (f φ))) →
      NPHard ZeroOneILP_problem)

    · -- Supply the NP-hardness of 3-SAT
      exact ThreeSAT_is_NPComplete.right

    · -- Supply the reduction and its proofs
      -- We must define the reduction function
      use (fun φ =>
        -- This function builds the matrix A and vector b from the 3-SAT formula φ
        -- 1. For each variable x, create a 0-1 variable in the ILP.
        -- 2. For each clause (l1 ∨ l2 ∨ l3), create an inequality.
        --    e.g., (x ∨ y ∨ ¬z) becomes x + y + (1-z) ≥ 1
        --    In our A*x <= b form, this is: -x - y + z ≤ 0
        (construct_ILP_from_3SAT φ))
      constructor
      · -- Proof that `construct_ILP_from_3SAT` runs in polynomial time
        sorry
      · -- Proof that the reduction is correct
        -- (φ is satisfiable ↔ the constructed ILP instance has a 0-1 solution)
        sorry

-- A graph G is defined over a vertex type V. `SimpleGraph V` is from mathlib.
-- An instance of Clique is a graph and a natural number k.
structure Clique.Instance (V : Type) [Fintype V] :=
  (G : SimpleGraph V)
  (k : ℕ)

-- The decision problem for Clique
def Clique_problem (V : Type) [Fintype V] : Language (Clique.Instance V) :=
  { P := fun inst =>
      -- There exists a subset of vertices 'S'
      ∃ (S : Finset V),
        -- Such that the size of S is k
        S.card = inst.k ∧
        -- And S is a clique (all pairs in S are adjacent)
        ∀ (u v : V), u ∈ S → v ∈ S → u ≠ v → inst.G.Adj u v
  }

-- Theorem: Clique is NP-complete
theorem Clique_is_NPComplete (V : Type) [Fintype V] : NPComplete (Clique_problem V) :=
by
  constructor
  · -- Part 1: Prove Clique is in NP
    -- We must show that a given subset S can be verified as a k-clique
    -- in polynomial time. This involves checking |S| = k and checking all
    -- pairs of vertices in S for adjacency.
    apply (NP_verifier_poly_time :
      NP (Clique_problem V))
    sorry -- This proof involves reasoning about O(k^2) checks.
  · -- Part 2: Prove Clique is NP-hard
    -- We show this by reducing 3-SAT to it.
    apply (NPHard_of_reduction :
      NPHard ThreeSAT_problem →
      (∃ (f : ThreeSAT.Formula ℕ → Clique.Instance V),
        (PolyTimeReduction f) ∧
        (∀ (φ : ThreeSAT.Formula ℕ),
          ThreeSAT_problem.P φ ↔ (Clique_problem V).P (f φ))) →
      NPHard (Clique_problem V))

    · -- Supply the NP-hardness of 3-SAT
      exact ThreeSAT_is_NPComplete.right

    · -- Supply the reduction and its proofs
      -- We must define the reduction function
      use (fun φ =>
        -- This function builds the graph G and k from the 3-SAT formula φ
        -- 1. Create one vertex for each literal in φ.
        -- 2. k = number of clauses in φ.
        -- 3. Add an edge between two vertices (literals) IF:
        --    a) They are in different clauses
        --    b) They are not opposites (e.g., not x and ¬x)
        (construct_Graph_from_3SAT φ))
      constructor
      · -- Proof that `construct_Graph_from_3SAT` runs in polynomial time
        sorry
      · -- Proof that the reduction is correct
        -- (φ is satisfiable ↔ the graph G has a k-clique)
        -- A k-clique in G corresponds to picking one literal from each
        -- clause that are all mutually compatible, which is a
        -- satisfying assignment.
        sorry

-- A Set Packing instance is a collection of Finsets (our 'sets')
-- and a number k.
structure SetPacking.Instance (U : Type) [Fintype U] :=
  (collection : Finset (Finset U)) -- A collection of sets
  (k : ℕ)

-- The decision problem for Set Packing
def SetPacking_problem (U : Type) [Fintype U] : Language (SetPacking.Instance U) :=
  { P := fun inst =>
      -- There exists a sub-collection 'S_pack'
      ∃ (S_pack : Finset (Finset U)),
        S_pack ⊆ inst.collection ∧
        S_pack.card = inst.k ∧
        -- And all sets in S_pack are pairwise disjoint
        ∀ (s1 ∈ S_pack), ∀ (s2 ∈ S_pack), s1 ≠ s2 →
          Disjoint s1 s2
  }

-- Theorem: Set Packing is NP-complete
theorem SetPacking_is_NPComplete (U V : Type) [Fintype U] [Fintype V] :
  NPComplete (SetPacking_problem U) :=
by
  constructor
  · -- Part 1: Prove Set Packing is in NP
    -- We must show that a given sub-collection S_pack can be verified
    -- in polynomial time. This involves checking its size and checking all
    -- O(k^2) pairs for disjointness.
    apply (NP_verifier_poly_time :
      NP (SetPacking_problem U))
    sorry -- Formalizing O(k^2) checks.
  · -- Part 2: Prove Set Packing is NP-hard
    -- We reduce Clique to Set Packing
    apply (NPHard_of_reduction :
      NPHard (Clique_problem V) → -- We use Clique's NP-hardness
      (∃ (f : Clique.Instance V → SetPacking.Instance U),
        (PolyTimeReduction f) ∧
        (∀ (cl : Clique.Instance V),
          (Clique_problem V).P cl ↔ (SetPacking_problem U).P (f cl))) →
      NPHard (SetPacking_problem U))

    · -- Supply the NP-hardness of Clique
      -- This comes from the `right` (NPHard) part of our previous theorem
      exact (Clique_is_NPComplete V).right

    · -- Supply the reduction and its proofs
      -- We must define the reduction function
      use (fun cl_inst =>
        -- This function builds a Set Packing instance from a Clique instance (G, k)
        -- 1. The new 'universe' U will be the set of *edges* in G.
        -- 2. For each *vertex* v in G, create a set containing all edges
        --    that are *incident* to v.
        -- 3. The new k is the same as the old k.
        (construct_SetPacking_from_Clique cl_inst))
      constructor
      · -- Proof that `construct_SetPacking_from_Clique` runs in poly time
        sorry
      · -- Proof that the reduction is correct
        -- (G has a k-clique ↔ The collection has a k-packing)
        -- A k-clique is k vertices where every pair is connected.
        -- The corresponding k sets will be disjoint *if and only if*
        -- no two vertices share an edge.
        -- Wait... this reduction is for *Independent Set*, not Clique.
        -- Let's use the reduction from your previous request:
        --
        -- **Correct Reduction (Clique to Set Packing):**
        -- 1. The universe U is the set of *non-edges* in G.
        -- 2. For each *vertex* v, create a set containing all *non-edges*
        --    incident to v.
        -- 3. The new k is the same k.
        --
        -- **Proof of correctness:**
        -- A k-clique is k vertices with *no* "non-edges" between them.
        -- A k-packing is k sets (vertices) that share no common elements.
        -- The elements are "non-edges".
        -- So, a k-packing is k vertices that share no "non-edges".
        -- This is the definition of a k-clique.
        sorry