OAI/Combinatorics/ParityLifts/SATRates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParityWL.Complexity.normalizeProgram line 7
2. def OAI.ParityWL.Complexity.satCode line 11
3. lemma OAI.ParityWL.Complexity.normalize_run line 13
4. lemma OAI.ParityWL.Complexity.poly_bit_input_bound line 19
5. lemma OAI.ParityWL.Complexity.decision_numeric_bound line 33
6. lemma OAI.ParityWL.Complexity.sat_code_rate line 74

   Source documentation

   The input polynomial degree is fixed once for the parser/compiler, independently of the sparsification threshold, target dimension, and the supplied WL machine.

   lemma sat_code_rate (p : FCode) (R : ℕ → ℝ) (r : ℝ) (hr : 0 ≤ r)
       (hR : ExpBound R r)
       (hp : ∀ {N : ℕ} (F : Formula N), ∃ b,
         RBEval p (treeEncode (minimizeList F.bitList)) (R N) (treeEncode b) ∧
         (b=true↔F.Satisfiable)) :
       ∀ ε : ℝ, 0<ε → ∃ C : ℝ, 0<C ∧
         SATTimeBound (satCode p).decision (fun N L =>
           C*(L+1 : ℝ)^(2*normalizeProgram.degree+2)*2^((2*r+ε)*N)) := by
   …

   Mentions: OAI.ParityWL.Complexity.FCode, OAI.ParityWL.Complexity.ExpBound, OAI.ParityWL.Complexity.Formula, OAI.ParityWL.Complexity.RBEval, OAI.ParityWL.Complexity.treeEncode, OAI.ParityWL.Complexity.minimizeList, OAI.ParityWL.Complexity.SATTimeBound, OAI.ParityWL.Complexity.satCode