ClauseGadget

formal source

 129/-! ## SAT Gadgets -/
 130
 131/-- A SAT clause encoded as CA cells -/
 132structure ClauseGadget (n : ℕ) where
 133  /-- Variable indices appearing in the clause -/
 134  variables : List (Fin n)
 135  /-- Negation flags for each variable -/
 136  negated : List Bool
 137  /-- Starting position on tape -/
 138  position : ℤ
 139  /-- Width of the gadget -/
 140  width : ℕ := 3 * variables.length + 2
 141
 142/-- Encode a SAT clause as CA cells -/
 143def encodeClause (g : ClauseGadget n) (assignment : Fin n → Bool) : Window g.width :=
 144  fun i =>
 145    if i.val < g.variables.length then
 146      let var_idx := g.variables.get! i.val
 147      let neg := g.negated.get! i.val
 148      let val := assignment var_idx
 149      if neg then (if val then .Zero else .One)
 150      else (if val then .One else .Zero)
 151    else if i.val = g.variables.length then
 152      .Gate  -- OR gate
 153    else
 154      .Wire
 155
 156/-- A full SAT instance encoded as CA tape -/
 157structure SATGadget where
 158  /-- Number of variables -/
 159  n : ℕ
 160  /-- Number of clauses -/
 161  m : ℕ
 162  /-- Clause gadgets -/