formalizing reductions

Stream: CSLib

[Frederick Pu]

I'm formalizing a reduction from 3SAT to 3DM. Right now the reduction is technically useless since we have no way of analyzing the time complexity of the reduction function. However, I think that the proof about the reduction functino being valid will be useful in the future when we are able to prove the time complexity of functions. I was wondering if there was anything similar already is in CSlib (or mathlib) and if I could get feedback on my formalism of 3SAT and 3DM as well as the reduction itself:

import Mathlib

structure CNF3 (n : Nat) where
  m : Nat
  C : Fin m → (Fin n × Bool) × (Fin n × Bool) × (Fin n × Bool)

def CNF3.sat (n : Nat) (s : CNF3 n) (x : Fin n → Bool) : Prop :=
  ∀ i : Fin s.m, let ((i, iv), (j, jv), (k, kv)) := (s.C i);
    x i == iv ∨ x j = jv ∨ x k = kv

def CNF3.occurances {n : Nat} (cnf : CNF3 n) (x : Fin n) : Nat :=
  ∑ i : Fin cnf.m,
    ((if (cnf.C i).1.1 == x then 1 else 0) +
    (if (cnf.C i).2.1.1 == x then 1 else 0) +
    (if (cnf.C i).2.2.1 == x then 1 else 0))

def CNF3.toOccurance₁ {n : Nat} (cnf : CNF3 n) (i : Fin cnf.m) : Fin (cnf.occurances (cnf.C i).1.1) := sorry

def CNF3.toOccurance₂ {n : Nat} (cnf : CNF3 n) (i : Fin cnf.m) : Fin (cnf.occurances (cnf.C i).2.1.1) := sorry

def CNF3.toOccurance₃ {n : Nat} (cnf : CNF3 n) (i : Fin cnf.m) : Fin (cnf.occurances (cnf.C i).2.2.1) := sorry

structure ThreeDM where
  (X Y Z : Type)
  (hX : Fintype X) (hY : Fintype Y) (hZ : Fintype Z)
  (T : Set (X × Y × Z))

def ThreeDM.sol (threedm : ThreeDM) (n : Nat) (M : Set (threedm.X × threedm.Y × threedm.Z)) : Prop :=
  M ⊆ threedm.T ∧ M.ncard = n ∧
    ∀ (xyz : threedm.X × threedm.Y × threedm.Z), xyz ∈ M → ∃! xyz' ∈ M, xyz.1 = xyz'.1 ∨ xyz.2.1 = xyz'.2.1 ∨ xyz.2.2 = xyz'.2.2

namespace ThreeDM

inductive ValueZ {n : Nat} (cnf : CNF3 n) where
| true (i : Fin n) (occ : Fin (cnf.occurances i)) : ValueZ cnf
| false (i : Fin n) (occ : Fin (cnf.occurances i)) : ValueZ cnf
deriving Fintype

inductive GroundingX {n : Nat} (cnf : CNF3 n) where
| valueGadget (i : Fin n) (occ : Fin (cnf.occurances i)) : GroundingX cnf
| clauseGadget (clause : Fin cnf.m) : GroundingX cnf
-- every clause needs `(3 - 1) = 2` garbage collectors (each clause is responsible for 3 variables each of which has one unaccounted for value (after value gadget), and only one value gets accounted for by clause gadget)
| garbageGadget (clause : Fin cnf.m) (garbageIdx : Fin 2) : GroundingX cnf
deriving Fintype


inductive GroundingY {n : Nat} (cnf : CNF3 n) where
| valueGadget (i : Fin n) (occ : Fin (cnf.occurances i)) : GroundingY cnf
| clauseGadget (clause : Fin cnf.m) : GroundingY cnf
-- every clause needs `(3 - 1) = 2` garbage collectors (each clause is responsible for 3 variables each of which has one unaccounted for value (after value gadget), and only one value gets accounted for by clause gadget)
| garbageGadget (clause : Fin cnf.m) (garbageIdx : Fin 2) : GroundingY cnf
deriving Fintype

#check Set.range

/-
  if (N x) is the number of clauses containing variable $x$ then each variable will require nodes 4(N x) for the variable gadget.
  we will also need an additional 2 * (num clauses) for the clause gadgets
  and 2 * (num remaining T or F), each clause will only use one T or F, the total number of T or F is ∑ 2(N x) so we will need ∑ 2(N x) - (num clauses) garbage gadgets.
  this gives a total of
  `(∑ 4(N x)) + 2 s.m +  (∑ 2(N x)) - s.m = 6 ∑ N x + s.m`
  but `∑ N x = 3 * (num clauses)`
  so we get `6 * (3 * s.m) + s.m = 19 * s.m`

  now for picking which nodes go in which sets. Note that in any gadget each throuple will consist of one point representing a value (T or F) and the other two points being used to link to other throuples in the gadget.
  Thus, we can think of  `Z` as being the value set and `X, Y` being the grounding types
-/
theorem threesat_reduction_threedm (n : Nat) (cnf : CNF3 n) :
    ∃ threedm : ThreeDM, (∃ x, cnf.sat n x) ↔ ∃ M, threedm.sol (19 * cnf.m) M := by
{
  let threedm : ThreeDM := {
    X := GroundingX cnf,
    Y := GroundingY cnf,
    Z := ValueZ cnf,
    hX := inferInstance,
    hY := inferInstance,
    hZ := inferInstance,
    T :=
      let valueGadgetTrue : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) :=
        Set.range (fun (⟨i, occ⟩ : Σ (i : Fin n), (Fin (cnf.occurances i))) => (.valueGadget i occ, .valueGadget i occ, .true i occ) )
      let valueGadgetFalse : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) :=
        Set.range (fun (⟨i, occ⟩ : Σ (i : Fin n), (Fin (cnf.occurances i))) => (.valueGadget i occ, .valueGadget i occ, .false i occ) )
      let valueGadget := valueGadgetTrue ∪ valueGadgetFalse

      let clauseGadget₁ : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) := Set.range (
        fun (i : Fin cnf.m) =>
          (.clauseGadget i,
           .clauseGadget i,
           if (cnf.C i).1.2 then
            .true (cnf.C i).1.1 (cnf.toOccurance₁ i)
          else
            .false (cnf.C i).1.1 (cnf.toOccurance₁ i)))
      let clauseGadget₂ : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) := Set.range (
        fun (i : Fin cnf.m) =>
        (.clauseGadget i,
         .clauseGadget i,
         if (cnf.C i).2.1.2 then
          .true (cnf.C i).2.1.1 (cnf.toOccurance₂ i)
        else
          .false (cnf.C i).2.1.1 (cnf.toOccurance₂ i)))
      let clauseGadget₃ : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) := Set.range (
        fun (i : Fin cnf.m) =>
        (.clauseGadget i,
         .clauseGadget i,
         if (cnf.C i).2.2.2 then
          .true (cnf.C i).2.2.1 (cnf.toOccurance₃ i)
        else
          .false (cnf.C i).2.2.1 (cnf.toOccurance₃ i)))
      let clauseGadget := clauseGadget₁ ∪ clauseGadget₂ ∪ clauseGadget₃

      -- for every clause and every variable attached to that clause, the point for tha variables at that clause is connected to both garbage collectors
      let garbageGadget₁ : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) := Set.range (
        fun (i : Fin cnf.m) =>
        (.garbageGadget i 0,
         .garbageGadget i 0,
         if (cnf.C i).1.2 then
            .true (cnf.C i).1.1 (cnf.toOccurance₁ i)
          else
            .false (cnf.C i).1.1 (cnf.toOccurance₁ i))
      ) ∪ Set.range (
        fun (i : Fin cnf.m) =>
        (.garbageGadget i 1,
         .garbageGadget i 1,
         if (cnf.C i).1.2 then
            .true (cnf.C i).1.1 (cnf.toOccurance₁ i)
          else
            .false (cnf.C i).1.1 (cnf.toOccurance₁ i))
      )
      let garbageGadget₂ : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) := Set.range (
        fun (i : Fin cnf.m) =>
        (.garbageGadget i 0,
         .garbageGadget i 0,
         if (cnf.C i).2.1.2 then
          .true (cnf.C i).2.1.1 (cnf.toOccurance₂ i)
        else
          .false (cnf.C i).2.1.1 (cnf.toOccurance₂ i))) ∪ Set.range (
        fun (i : Fin cnf.m) =>
        (.garbageGadget i 1,
         .garbageGadget i 1,
         if (cnf.C i).2.1.2 then
          .true (cnf.C i).2.1.1 (cnf.toOccurance₂ i)
        else
          .false (cnf.C i).2.1.1 (cnf.toOccurance₂ i)))
      let garbageGadget₃ : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) := Set.range (
        fun (i : Fin cnf.m) =>
        (.garbageGadget i 0,
         .garbageGadget i 0,
         if (cnf.C i).2.2.2 then
          .true (cnf.C i).2.2.1 (cnf.toOccurance₃ i)
        else
          .false (cnf.C i).2.2.1 (cnf.toOccurance₃ i))) ∪ Set.range (
        fun (i : Fin cnf.m) =>
        (.garbageGadget i 1,
         .garbageGadget i 1,
         if (cnf.C i).2.2.2 then
          .true (cnf.C i).2.2.1 (cnf.toOccurance₃ i)
        else
          .false (cnf.C i).2.2.1 (cnf.toOccurance₃ i)))
      let garbageGadget : Set (GroundingX cnf × GroundingY cnf × ValueZ cnf) := garbageGadget₁ ∪ garbageGadget₂ ∪ garbageGadget₃
      valueGadget ∪ clauseGadget ∪ garbageGadget

  }
  sorry
}

[Frederick Pu]

PS, im basing this off of the MIT open courseware lecture: https://www.youtube.com/watch?v=eHZifpgyH_4&t=2786s

[Nadim Farhat]

not sure whats the overlap but early on the idea was to formalize this book https://mitpress.mit.edu/9780262046305/introduction-to-algorithms/ , also found this https://github.com/leanprover/cslib/blob/main/CslibTests/ReductionSystem.lean

[Frederick Pu]

does this formalize a notion of runtime complexity too?