def
definition
def or abbrev
sat_eval_time
show as:
view Lean formalization →
formal statement (Lean)
172noncomputable def sat_eval_time (n m : ℕ) : ℕ :=
proof body
Definition body.
173 -- Depth of the clause evaluation tree: O(log m) for m clauses
174 -- Width propagation: O(n^{1/3}) for n variables arranged optimally
175 -- Total: O(n^{1/3} · log(n·m))
176 Nat.ceil (Real.rpow n (1/3) * Real.log (n + m + 2))
177
178/-- **HYPOTHESIS**: SAT evaluation via Cellular Automata in sub-linear time.
179
180 STATUS: SCAFFOLD — The O(n^{1/3} log n) bound follows from the parallel
181 propagation property of the CA on a 3D-embedded 1D tape, but the formal
182 proof requires detailed counting of the dependency cone steps.
183
184 TODO: Formally prove the O(n^{1/3} log n) bound. -/