Prove2Me

kk-SAT under bounded variable occurrence for a finite subfamily of clauses over arbitrary variable and index sets

Proved
QLLL.SAT.exists_assignment_of_finset

by sattath · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

k-satlovasz-local-lemmaquantum-lll

A clause is a disjunction of literals over boolean variables, and an assignment satisfies it if at least one literal evaluates to true. Let V\mathcal{V} be an arbitrary set of variables and let (Ci)i∈I(C_i)_{i \in I} be clauses over V\mathcal{V} indexed by an arbitrary set II. Let T⊆IT \subseteq I be finite, and let k≥1k \ge 1 and D≥1D \ge 1 be integers such that:

  1. every clause CiC_i with i∈Ti \in T involves exactly kk distinct variables;
  2. every variable occurs in at most DD of the clauses CiC_i with i∈Ti \in T;
  3. D⋅e⋅k≤2kD \cdot e \cdot k \le 2^{k}.

Then there is an assignment a:V→{0,1}a : \mathcal{V} \to \{0,1\} satisfying every CiC_i with i∈Ti \in T.

This transports Corollary 2 of Ambainis, Kempe and Sattath to arbitrary variable and index types, with hypotheses required only on TT. It is the finite step in the compactness proof of the infinite version QLLL.SAT.exists_assignment_forall.

Preamble
import Definitions.Def_QLLL_LocalLemma_Basic
import Definitions.Def_QLLL_Classical_KSAT
import Definitions.Def_QLLL_Classical_InfiniteKSAT
import Mathlib
import Std.Sat.CNF

open QLLL
open QLLL.SAT
open Finset Std.Sat
Formal statement
theorem QLLL.SAT.exists_assignment_of_finset {V ι : Type*} [DecidableEq V]
    (C : ι → CNF.Clause V) (T : Finset ι) (k D : ℕ) (hk : 1 ≤ k) (hD1 : 1 ≤ D)
    (hvars : ∀ i ∈ T, (clauseVars' (C i)).card = k)
    (hdeg : ∀ v : V, (T.filter fun i => v ∈ clauseVars' (C i)).card ≤ D)
    (hDk : (D : ℝ) * (Real.exp 1 * k) ≤ 2 ^ k) :
    ∃ a : V → Bool, ∀ i ∈ T, CNF.Clause.eval a (C i) = true := by sorry
Source
Not in the paper; a transport of Corollary 2 to arbitrary variable and index types. Formalization companion to Ambainis, Kempe and Sattath, A Quantum Lovász Local Lemma, arXiv:0911.1696; see the blueprint https://sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint/

View graph