Isolated directions of a set of bit strings

For a set S of bit strings of length n and σ ∈ S, the isolation of σ is the number of coordinates i such that flipping coordinate i of σ leaves S (Cslib.BitString.isolation). Every nonempty S satisfies 2^n ≤ ∑_{σ ∈ S} 2^{isolation S σ} (Cslib.BitString.two_pow_le_sum_two_pow_isolation): a single point is isolated in all n directions, and in general the bound follows by induction on n, splitting S by its first coordinate. This is the counting step of the PPZ analysis for formulas with several satisfying assignments Paturi, Pudlák, Zane.

Main definitions

• Cslib.BitString.isolation: the number of directions in which σ is isolated in S.

Main results

• Cslib.BitString.two_pow_le_sum_two_pow_isolation: 2^n ≤ ∑_{σ ∈ S} 2^{isolation S σ}.

References

• R. Paturi, P. Pudlák, F. Zane, Satisfiability Coding Lemma

def Cslib.BitString.isolation {n : ℕ} (S : Finset (Fin n → Bool)) (σ : Fin n → Bool) : ℕ

The number of coordinates i such that flipping coordinate i of σ leaves S.

def Cslib.BitString.slice {n : ℕ} (S : Finset (Fin (n + 1) → Bool)) (b : Bool) : Finset (Fin n → Bool)

The strings of S with first coordinate b, with that coordinate removed.

theorem Cslib.BitString.mem_slice {n : ℕ} {S : Finset (Fin (n + 1) → Bool)} {b : Bool} {τ : Fin n → Bool} : τ ∈ slice S b ↔ Fin.cons b τ ∈ S

theorem Cslib.BitString.isolation_cons_ge {n : ℕ} (S : Finset (Fin (n + 1) → Bool)) (b : Bool) (τ : Fin n → Bool) : (isolation (slice S b) τ + if Fin.cons (!b) τ ∈ S then 0 else 1) ≤ isolation S (Fin.cons b τ)

The isolation of Fin.cons b τ in S is at least the isolation of τ in its slice, plus one if flipping the first coordinate leaves S.

theorem Cslib.BitString.two_pow_le_sum_two_pow_isolation {n : ℕ} (S : Finset (Fin n → Bool)) : S.Nonempty → 2 ^ n ≤ ∑ σ ∈ S, 2 ^ isolation S σ

The isolation inequality: every nonempty set S of bit strings of length n satisfies 2^n ≤ ∑_{σ ∈ S} 2^{isolation S σ}.