encodeClause

formal source

 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 -/
 163  clauses : List (ClauseGadget n)
 164  /-- Variable assignment cells -/
 165  var_positions : Fin n → ℤ
 166  /-- Output cell position -/
 167  output_position : ℤ
 168  /-- Total tape width used -/
 169  total_width : ℕ := n + 3 * m + 10
 170
 171/-- The evaluation time for a SAT instance with n variables and m clauses -/
 172noncomputable def sat_eval_time (n m : ℕ) : ℕ :=
 173  -- Depth of the clause evaluation tree: O(log m) for m clauses