$k$ -SAT under bounded variable occurrence: a common satisfying assignment for a finite family of clauses

Proved

QLLL.SAT.exists_forall_clause_eval

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 $C_1, \dots, C_m$ be clauses over the variables $x_1, \dots, x_V$ , each involving exactly $k$ distinct variables, with $k \ge 1$ . Let $D \ge 1$ be an integer such that every variable occurs in at most $D$ of the clauses, and suppose

D \cdot e \cdot k \ \le\ 2^{k}.

Then there is an assignment $a \in \{0,1\}^{V}$ satisfying every $C_i$ .

This is the combinatorial core of Corollary 2 of Ambainis, Kempe and Sattath, for an indexed family of clauses rather than a formula. It is used for the formula version QLLL.SAT.sat_of_degree_le and for the infinite version QLLL.SAT.exists_assignment_forall.

Formalization Note Clauses are Std.Sat.CNF.Clause (Fin V) and an assignment is a function Fin V → Bool.

Preamble

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

open QLLL
open QLLL.SAT
open Finset Std.Sat
variable (Ω : Type*) [Fintype Ω] [DecidableEq Ω] [Nonempty Ω]
variable {V : ℕ}

Formal statement

theorem QLLL.SAT.exists_forall_clause_eval {V m : ℕ} (C : Fin m → CNF.Clause (Fin V))
    (k D : ℕ) (hk : 1 ≤ k) (hD1 : 1 ≤ D)
    (hvars : ∀ i, (clauseVars (C i)).card = k)
    (hdeg : ∀ v : Fin V, (univ.filter fun i => v ∈ clauseVars (C i)).card ≤ D)
    (hDk : (D : ℝ) * (Real.exp 1 * k) ≤ 2 ^ k) :
    ∃ a : Asg V, ∀ i, CNF.Clause.eval a (C i) = true := by sorry

Source

A. Ambainis, J. Kempe, O. Sattath, A Quantum Lovász Local Lemma, J. ACM 59(5):24 (2012), arXiv:0911.1696 (numbering of the arXiv version), Corollary 2

View graph

kkk-SAT under bounded variable occurrence: a common satisfying assignment for a finite family of clauses

$k$ -SAT under bounded variable occurrence: a common satisfying assignment for a finite family of clauses