The satisfiability coding lemma

The coding lemma of Paturi, Pudlák and Zane [PPZ99], with exact sums over all orders of the variables in place of probabilities. Fix a formula φ in conjunctive normal form over N variables and an order σ of the variables. A variable v is forced on a solution x (CNF.forced) when some clause contains the literal of v true under x and all its other literals are on earlier variables and false under x. The words agreeing with a solution x off its forced variables are disjoint for distinct solutions: at the first variable where two solutions differ, a clause forcing it in one of them is false under the other (CNF.disjoint_agreeOffForced). Hence ∑ₓ 2 ^ |forced σ x| ≤ 2 ^ N for every order (CNF.sum_two_pow_card_forced_le), and by the inequality of arithmetic and geometric means the same holds with the average number of forced variables over all orders in the exponent (CNF.sum_two_rpow_average_card_forced_le).

If every clause has at most k literals and x is isolated in direction i (flipping bit i of x gives no solution), some clause is critical for i (CNF.exists_critical), and i is forced whenever it comes last among the variables of that clause, for at least a 1 / k fraction of the orders (CNF.factorial_le_mul_card_filter_mem_forced, from Equiv.Perm.card_mul_card_filter_forall_le_eq_factorial). Hence ∑ₓ 2 ^ (ι(x) / k) ≤ 2 ^ N, where ι(x) is the number of directions in which x is isolated (CNF.sum_two_rpow_card_isolated_div_le), and a k-CNF has at most 2 ^ ((1 - 1 / k) N) solutions isolated in every direction (CNF.card_isolatedInputs_mul_two_rpow_le).

Main definitions

• Cslib.Logic.PL.CNF.forced: the variables forced on a solution for an order of the variables.

Main results

• Cslib.Logic.PL.CNF.sum_two_pow_card_forced_le: the coding bound for one order.
• Cslib.Logic.PL.CNF.sum_two_rpow_average_card_forced_le: the coding lemma.
• Cslib.Logic.PL.CNF.sum_two_rpow_card_isolated_div_le: the coding lemma for k-CNFs.
• Cslib.Logic.PL.CNF.card_isolatedInputs_mul_two_rpow_le: few isolated solutions.

References

• R. Paturi, P. Pudlák, F. Zane, Satisfiability coding lemma

def Cslib.Logic.PL.CNF.Forces {N : ℕ} (σ : Equiv.Perm (Fin N)) (x : BitString N) (c : Clause (Fin N)) (v : Fin N) : Prop

The clause c forces v on x for the order σ: it contains the literal of v true under x, and all its other literals are on variables before v (in the order σ) and false under x. This is the deletion rule of Paturi, Pudlák and Zane: such a clause is critical for v at x and v comes last among its variables, so the decoder meets it as a unit clause on v. A clause also containing the literal of v false under x forces nothing, as the decoder would not see a unit clause there; the definition rules it out, since that literal would need σ v < σ v.

@[instance_reducible]

instance Cslib.Logic.PL.CNF.instDecidableForces {N : ℕ} (σ : Equiv.Perm (Fin N)) (x : BitString N) (c : Clause (Fin N)) (v : Fin N) : Decidable (Forces σ x c v)

def Cslib.Logic.PL.CNF.forced {N : ℕ} (φ : CNF (Fin N)) (σ : Equiv.Perm (Fin N)) (x : BitString N) : Finset (Fin N)

The variables forced on x for the order σ: those forced by some clause.

@[simp]

theorem Cslib.Logic.PL.CNF.mem_forced {N : ℕ} {φ : CNF (Fin N)} {σ : Equiv.Perm (Fin N)} {x : BitString N} {v : Fin N} : v ∈ φ.forced σ x ↔ ∃ c ∈ φ, Forces σ x c v

def Cslib.Logic.PL.CNF.agreeOffForced {N : ℕ} (φ : CNF (Fin N)) (σ : Equiv.Perm (Fin N)) (x : BitString N) : Finset (BitString N)

The words agreeing with x outside the variables forced on x.

theorem Cslib.Logic.PL.CNF.disjoint_agreeOffForced {N : ℕ} {φ : CNF (Fin N)} {σ : Equiv.Perm (Fin N)} {x x' : BitString N} (hx : eval x φ = true) (hx' : eval x' φ = true) (hne : x ≠ x') : Disjoint (φ.agreeOffForced σ x) (φ.agreeOffForced σ x')

The words agreeing with distinct solutions off their forced variables are disjoint: at the first variable, in the order σ, where two solutions differ, one of them is forced, and the clause forcing it is false under the other solution.

theorem Cslib.Logic.PL.CNF.sum_two_pow_card_forced_le {N : ℕ} (φ : CNF (Fin N)) (σ : Equiv.Perm (Fin N)) : ∑ x : BitString N with eval x φ = true, 2 ^ (φ.forced σ x).card ≤ 2 ^ N

The coding bound for one order: the solutions x of φ satisfy ∑ₓ 2 ^ |forced σ x| ≤ 2 ^ N.

Isolated directions are forced often

def Cslib.Logic.PL.CNF.Critical {N : ℕ} (x : BitString N) (c : Clause (Fin N)) (i : Fin N) : Prop

The clause c is critical for the direction i at x: it contains the literal of i true under x, and all its other literals are on other variables and false under x. Flipping bit i of x falsifies a critical clause.

@[instance_reducible]

instance Cslib.Logic.PL.CNF.instDecidableCritical {N : ℕ} (x : BitString N) (c : Clause (Fin N)) (i : Fin N) : Decidable (Critical x c i)

theorem Cslib.Logic.PL.CNF.exists_critical {N : ℕ} {φ : CNF (Fin N)} {x : BitString N} {i : Fin N} (hx : eval x φ = true) (hi : eval (Function.update x i !x i) φ = false) : ∃ c ∈ φ, Critical x c i

A direction i in which a solution x is isolated has a critical clause.

theorem Cslib.Logic.PL.CNF.critical_congr {N : ℕ} {x : BitString N} {i : Fin N} {c c' : Clause (Fin N)} (h : ∀ (l : Literal (Fin N)), l ∈ c ↔ l ∈ c') : Critical x c i ↔ Critical x c' i

Criticality depends only on the literals of the clause.

theorem Cslib.Logic.PL.CNF.card_filter_critical_prod_le {N : ℕ} (c : Clause (Fin N)) : {p : BitString N × Fin N | Critical p.1 c p.2}.card ≤ (List.map Prod.fst c).toFinset.card * 2 ^ (N - (List.map Prod.fst c).toFinset.card)

A clause with v variables is critical for at most v 2 ^ (N - v) pairs of an input and a direction.

theorem Cslib.Logic.PL.CNF.factorial_le_mul_card_filter_mem_forced {N : ℕ} {φ : CNF (Fin N)} {k : ℕ} (hk : ∀ c ∈ φ, List.length c ≤ k) {x : BitString N} {i : Fin N} (hx : eval x φ = true) (hi : eval (Function.update x i !x i) φ = false) : N.factorial ≤ k * {σ : Equiv.Perm (Fin N) | i ∈ φ.forced σ x}.card

Isolated directions are forced often. If every clause of φ has at most k literals, every direction i in which a solution x is isolated is forced for at least a 1 / k fraction of the orders.

Averaging over the orders

theorem Cslib.Logic.PL.CNF.sum_two_rpow_average_card_forced_le {N : ℕ} (φ : CNF (Fin N)) : ∑ x : BitString N with eval x φ = true, 2 ^ ((∑ σ : Equiv.Perm (Fin N), ↑(φ.forced σ x).card) / ↑N.factorial) ≤ 2 ^ N

The coding lemma Paturi, Pudlák and Zane, Lemma 1 and Fact 3: with E(x) the average, over all N! orders, of the number of variables forced on a solution x, the solutions satisfy ∑ₓ 2 ^ E(x) ≤ 2 ^ N.

theorem Cslib.Logic.PL.CNF.sum_two_rpow_card_isolated_div_le {N : ℕ} {φ : CNF (Fin N)} {k : ℕ} (hk1 : 1 ≤ k) (hk : ∀ c ∈ φ, List.length c ≤ k) : ∑ x : BitString N with eval x φ = true, 2 ^ (↑{i : Fin N | eval (Function.update x i !x i) φ = false}.card / ↑k) ≤ 2 ^ N

The coding lemma for formulas of width k Paturi, Pudlák and Zane, Lemma 2: if every clause has at most k ≥ 1 literals, the solutions x satisfy ∑ₓ 2 ^ (ι(x) / k) ≤ 2 ^ N, where ι(x) is the number of directions in which x is isolated.

theorem Cslib.Logic.PL.CNF.card_isolatedInputs_mul_two_rpow_le {N : ℕ} {φ : CNF (Fin N)} {k : ℕ} (hk1 : 1 ≤ k) (hk : ∀ c ∈ φ, List.length c ≤ k) : ↑(BitString.isolatedInputs (fun (σ : Fin N → Bool) => eval σ φ) true).card * 2 ^ (↑N / ↑k) ≤ 2 ^ N

Few isolated solutions Paturi, Pudlák and Zane, Lemma 4: a formula whose clauses have at most k ≥ 1 literals has at most 2 ^ ((1 - 1 / k) N) solutions isolated in every direction.

Weights of solutions

noncomputable def Cslib.Logic.PL.CNF.critWidth {N : ℕ} (φ : CNF (Fin N)) (x : BitString N) (i : Fin N) : ℕ

The number of variables of a shortest clause critical for the direction i at x, or 0 if no clause is.

theorem Cslib.Logic.PL.CNF.exists_critical_card_eq_critWidth {N : ℕ} {φ : CNF (Fin N)} {x : BitString N} {i : Fin N} (h : ∃ c ∈ φ, Critical x c i) : ∃ c ∈ φ, Critical x c i ∧ (List.map Prod.fst c).toFinset.card = φ.critWidth x i

theorem Cslib.Logic.PL.CNF.critWidth_pos {N : ℕ} {φ : CNF (Fin N)} {x : BitString N} {i : Fin N} (h : ∃ c ∈ φ, Critical x c i) : 0 < φ.critWidth x i

theorem Cslib.Logic.PL.CNF.sum_two_rpow_sum_inv_critWidth_le {N : ℕ} (φ : CNF (Fin N)) : ∑ x : BitString N with eval x φ = true, 2 ^ ∑ i : Fin N, 1 / ↑(φ.critWidth x i) ≤ 2 ^ N

The weighted coding lemma, after Paturi, Pudlák and Zane, Lemma 5: the solutions x of any formula satisfy ∑ₓ 2 ^ w(x) ≤ 2 ^ N, where the weight w(x) = ∑ᵢ 1 / critWidth φ x i sums, over the directions in which x is isolated, the inverse number of variables of a shortest critical clause.

theorem Cslib.Logic.PL.CNF.card_filter_le_sum_inv_critWidth_mul_two_rpow_le {N : ℕ} (φ : CNF (Fin N)) (μ : ℝ) : ↑{x : BitString N | eval x φ = true ∧ μ ≤ ∑ i : Fin N, 1 / ↑(φ.critWidth x i)}.card * 2 ^ μ ≤ 2 ^ N

Few solutions of large weight Paturi, Pudlák and Zane, Lemma 5: at most 2 ^ (N - μ) solutions have weight at least μ.