`three_sat_runtime_prop`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.Runtime
domain: Complexity
line: 38 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.Runtime on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

  35
  36/-- Target bound for the full 3-SAT algorithm.
  37    Total TM time is bounded by O(n^{11/3} log n). -/
  38def three_sat_runtime_prop (n : Nat) : Prop :=
  39  ∃ c : ℝ, c > 0 ∧ (n : ℝ)^(11/3 : ℝ) * Real.log (n + 2) ≤ c * (n : ℝ)^4
  40
  41
  42end SAT
  43end Complexity
  44end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.