The satisfiability coding lemma -- proofs

Internal proofs for Complexitylib.Circuits.KCNF.Coding.

On a solution x of ψ, the decoder for the order σ recovers x from every input y that agrees with x off the forced variables (decode_eq_of_agree). So the sets of such inputs are disjoint for distinct solutions, and the sum of 2 ^ |forced σ x| over the solutions is at most 2 ^ N. Averaging over all orders and applying Jensen's inequality to t ↦ 2 ^ t gives the bound with the average number of forced variables in the exponent.

For a clause set of width k, every isolated direction i of a solution x has a clause whose only true literal under x is on i; then i is forced whenever σ places i after the other variables of that clause, which happens for at least a 1/k fraction of the orders (card_lastIn_mul_card).

theorem Complexity.ClauseSet.Coding.eval_eq_true_of_others_false {N : ℕ} {C : Finset (Literal N)} {x : BitString N} (hsat : ∃ l ∈ C, l.eval x = true) {l : Literal N} (hothers : ∀ l' ∈ C, l' ≠ l → l'.eval x = false) : l.eval x = true

In a satisfied clause whose other literals are false, the remaining literal is true.

theorem Complexity.ClauseSet.Coding.fires_congr {N : ℕ} {σ : Equiv.Perm (Fin N)} {z x : BitString N} {v : Fin N} (hzx : ∀ (u : Fin N), σ u < σ v → z u = x u) (C : Finset (Literal N)) (l : Literal N) : (∀ l' ∈ C, l' ≠ l → σ l'.var < σ v ∧ l'.eval z = false) ↔ ∀ l' ∈ C, l' ≠ l → σ l'.var < σ v ∧ l'.eval x = false

The firing condition only reads the variables placed before v.

theorem Complexity.ClauseSet.Coding.decodeValue_eq {N : ℕ} {ψ : ClauseSet N} {σ : Equiv.Perm (Fin N)} {x z : BitString N} {v : Fin N} {b : Bool} (hx : ψ.Sat x) (hzx : ∀ (u : Fin N), σ u < σ v → z u = x u) (hb : v ∉ ψ.forced σ x → b = x v) : ψ.decodeValue σ z v b = x v

One decoding step: on a partial assignment that agrees with the solution x before v, and with an input bit that is x v unless v is forced, the decoder gives v its value in x.

theorem Complexity.ClauseSet.Coding.decodeUpTo_eq {N : ℕ} {ψ : ClauseSet N} {σ : Equiv.Perm (Fin N)} {x y : BitString N} (hx : ψ.Sat x) (hy : ∀ v ∉ ψ.forced σ x, y v = x v) (p : ℕ) : p ≤ N → ∀ (v : Fin N), ψ.decodeUpTo σ y p v = if ↑(σ v) < p then x v else y v

The decoder invariant. After p positions, the decoder holds the solution's values at the positions before p and the input's values elsewhere.

theorem Complexity.ClauseSet.Coding.decode_eq_of_agree {N : ℕ} {ψ : ClauseSet N} {σ : Equiv.Perm (Fin N)} {x y : BitString N} (hx : ψ.Sat x) (hy : ∀ v ∉ ψ.forced σ x, y v = x v) : ψ.decode σ y = x

Decoding. On every input that agrees with a solution x off its forced variables, the decoder outputs x.

theorem Complexity.ClauseSet.Coding.sum_two_pow_forced_le {N : ℕ} (ψ : ClauseSet N) (σ : Equiv.Perm (Fin N)) : ∑ x ∈ ψ.solutions, 2 ^ (ψ.forced σ x).card ≤ 2 ^ N

The coding bound for one order.

theorem Complexity.ClauseSet.Coding.sum_two_rpow_average_forced_le {N : ℕ} (ψ : ClauseSet N) : ∑ x ∈ ψ.solutions, 2 ^ ((∑ σ : Equiv.Perm (Fin N), ↑(ψ.forced σ x).card) / ↑N.factorial) ≤ 2 ^ N

The coding bound, averaged over all orders. With the average number of forced variables in the exponent, the sum over the solutions is at most 2 ^ N (Jensen's inequality).

Isolated directions are forced often

def Complexity.ClauseSet.Coding.lastIn {N : ℕ} (V : Finset (Fin N)) (j : Fin N) : Finset (Equiv.Perm (Fin N))

The orders that place j after every other element of V.

Equations

• Complexity.ClauseSet.Coding.lastIn V j = {σ : Equiv.Perm (Fin N) | ∀ u ∈ V, u ≠ j → σ u < σ j}

theorem Complexity.ClauseSet.Coding.card_lastIn_eq {N : ℕ} {V : Finset (Fin N)} {i j : Fin N} (hi : i ∈ V) (hj : j ∈ V) : (lastIn V j).card = (lastIn V i).card

theorem Complexity.ClauseSet.Coding.card_lastIn_mul_card {N : ℕ} {V : Finset (Fin N)} {i : Fin N} (hi : i ∈ V) : (lastIn V i).card * V.card = N.factorial

Symmetry of orders. Exactly a 1/|V| fraction of the orders place a given element of V after the others.

theorem Complexity.ClauseSet.Coding.exists_critical_clause {N : ℕ} {ψ : ClauseSet N} {x : BitString N} {i : Fin N} (hx : ψ.Sat x) (hi : i ∈ isolatedDirections ψ.solutions x) : ∃ C ∈ ψ, ∃ l ∈ C, l.var = i ∧ ∀ l' ∈ C, l' ≠ l → l'.var ≠ i ∧ l'.eval x = false

An isolated direction of a solution has a critical clause: a clause whose only true literal under x is a literal on that direction.

theorem Complexity.ClauseSet.Coding.card_isolated_mul_factorial_le {N : ℕ} {ψ : ClauseSet N} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) {x : BitString N} (hx : ψ.Sat x) : (isolatedDirections ψ.solutions x).card * N.factorial ≤ k * ∑ σ : Equiv.Perm (Fin N), (ψ.forced σ x).card

Isolated directions are forced on average. For a clause set of width at most k, the number of isolated directions of a solution times N! is at most k times the total number of forced variables over all orders.

theorem Complexity.ClauseSet.Coding.sum_two_rpow_isolated_div_le {N : ℕ} {ψ : ClauseSet N} {k : ℕ} (hk1 : 1 ≤ k) (hk : ∀ C ∈ ψ, C.card ≤ k) : ∑ x ∈ ψ.solutions, 2 ^ (↑(isolatedDirections ψ.solutions x).card / ↑k) ≤ 2 ^ N

The coding lemma for k-CNFs. For a clause set of width at most k ≥ 1, the sum over its solutions of 2 ^ (ι(x)/k), ι(x) the number of isolated directions, is at most 2 ^ N.