structure AlgorithmicLLL.FixSystem (Clause : Type u_3) (State : Type u_4) : Type (max u_3 u_4)

A FixSystem abstracts the structure underlying Moser's algorithm. It consists of clauses and states, a predicate satisfied saying when a clause holds in a state, a fix operation that repairs a clause, the guarantee that fix c makes c satisfied, and the invariant that fix c preserves all currently satisfied clauses.

• satisfied : Clause → State → Prop
• fix : Clause → State → State
• fix_makes_satisfied (c : Clause) (s : State) : self.satisfied c (self.fix c s)
• fix_preserves_satisfied (c d : Clause) (s : State) : self.satisfied d s → self.satisfied d (self.fix c s)

def AlgorithmicLLL.IsValidOuterLoop {Clause : Type u_1} {State : Type u_2} (sys : FixSystem Clause State) : List Clause → State → Prop

IsValidOuterLoop sys cs s says that the list of clauses cs is a valid execution trace of the outer loop of Moser's algorithm starting from state s: each successive clause is unsatisfied at the moment it is visited and then fixed.

theorem AlgorithmicLLL.outer_loop_nodup {Clause : Type u_1} {State : Type u_2} (sys : FixSystem Clause State) [DecidableEq Clause] (cs : List Clause) (s : State) (h : IsValidOuterLoop sys cs s) : cs.Nodup

Any valid outer-loop trace contains each clause at most once: once a clause is fixed it remains satisfied, so it can never be the unsatisfied clause selected at a later step.

structure AlgorithmicLLL.KCNF : Type

A KCNF instance: $k$-CNF formula data with numVars Boolean variables, numClauses clauses each of width $k \ge 3$, and maxShared bounding the number of clauses sharing a variable with a given clause.

• numVars : ℕ
• numClauses : ℕ
• k : ℕ
• maxShared : ℕ
• hk : 3 ≤ self.k
• hn : 0 < self.numVars

structure AlgorithmicLLL.MoserKCNFextends AlgorithmicLLL.KCNF : Type

A MoserKCNF is a KCNF satisfying Moser's sharing condition $\text{maxShared} \le 2^{k-3}$, the hypothesis under which Moser's algorithm provably finds a satisfying assignment.

• numVars : ℕ
• numClauses : ℕ
• k : ℕ
• maxShared : ℕ
• hk : 3 ≤ self.k
• hn : 0 < self.numVars
• hshared : self.maxShared ≤ 2 ^ (self.k - 3)

def AlgorithmicLLL.numAssignments (n : ℕ) : ℕ

The number $2^n$ of Boolean assignments on $n$ variables.

def AlgorithmicLLL.numExecutionTraces (k ℓ : ℕ) : ℕ

Upper bound $2^{\ell(k-1)+1}$ on the number of execution traces of Moser's algorithm of length $\ell$ on a $k$-CNF formula, used in the entropy-compression argument.

def AlgorithmicLLL.failureBound (n k ℓ : ℕ) : ℕ

Combined failure bound $2^n \cdot 2^{\ell(k-1)+1}$ from entropy compression: the count of (assignment, trace) pairs available to encode failing executions.

theorem AlgorithmicLLL.failureBound_eq_pow (n k ℓ : ℕ) : failureBound n k ℓ = 2 ^ (n + (ℓ * (k - 1) + 1))

Rewrites failureBound n k ℓ as a single power of $2$: $2^{n + \ell(k-1) + 1}$.

theorem AlgorithmicLLL.exponent_identity (n k ℓ : ℕ) (hk : 1 ≤ k) : n + (ℓ * (k - 1) + 1) + ℓ = k * ℓ + (n + 1)

Arithmetic identity used to compare exponents in the failure-probability bound: $n + \ell(k-1) + 1 + \ell = k\ell + n + 1$, valid whenever $k \ge 1$.

theorem AlgorithmicLLL.entropy_compression_card_bound (φ : MoserKCNF) (ℓ : ℕ) (hℓ : 0 < ℓ) : ∃ (failingSet : Finset (Fin (2 ^ (φ.k * ℓ)))), failingSet.card ≤ failureBound φ.numVars φ.k ℓ

Entropy-compression cardinality bound: among the $2^{k\ell}$ possible random tapes of length $k\ell$, the set on which Moser's algorithm runs for $\ell$ steps without finishing has cardinality at most failureBound φ.numVars φ.k ℓ.

theorem AlgorithmicLLL.failure_prob_bound_nat (n k ℓ numFailing : ℕ) (h_inj : numFailing ≤ failureBound n k ℓ) (hk : 1 ≤ k) : numFailing * 2 ^ ℓ ≤ 2 ^ (k * ℓ) * 2 ^ (n + 1)

Natural-number version of the failure-probability bound: $\text{numFailing} \cdot 2^\ell \le 2^{k\ell} \cdot 2^{n+1}$ whenever the failing count is bounded by failureBound n k ℓ.

theorem AlgorithmicLLL.fix_recursive_calls_prob_bound (φ : MoserKCNF) (ℓ : ℕ) (hℓ : 0 < ℓ) : ∃ (failingSet : Finset (Fin (2 ^ (φ.k * ℓ)))), failingSet.card ≤ failureBound φ.numVars φ.k ℓ ∧ ↑failingSet.card / 2 ^ (φ.k * ℓ) ≤ 2 ^ (φ.numVars + 1) / 2 ^ ℓ

Theorem 6.6.6 (Moser's algorithm on $k$-CNF). Under the sharing condition $\text{maxShared} \le 2^{k-3}$, the probability that Moser's Fix procedure makes more than $\ell$ recursive calls is bounded by $2^{n+1}/2^\ell$, which decays geometrically in $\ell$ and so the algorithm almost surely terminates.