Formulas without large subcubes of solutions have few solutions

A move of a solution x of a clause set ψ is a nonempty set T of variables such that x with the bits in T flipped (BitString.flipOn) is again a solution; two moves are separated when no clause meets both. Separated moves combine freely (ClauseSet.flipOn_biUnion_mem_solutions_of_separated), so in a clause set whose variables have at most Δ neighbours in the co-occurrence graph and whose solutions contain no subcube of dimension D (ContainsSubcube), every solution has at most (D - 1)(Δ + 1) directions in which it is not isolated (ClauseSet.card_compl_isolatedDirections_le). The satisfiability coding lemma then bounds the solutions (ClauseSet.card_solutions_le_of_neighbors), and after sparsification every formula of width k is a union of at most 2 ^ (ε N) such pieces: a formula of width k over N variables whose solutions contain no subcube of dimension D has at most 2 ^ ((1 - 1 / k + ε) N + C D) solutions (ClauseSet.card_solutions_le_of_not_containsSubcube).

The exponent 1 - 1 / k cannot be improved, already for D = 1: requiring even parity on each of N / k disjoint blocks of k variables gives 2 ^ ((1 - 1 / k) N) solutions, no two of which are neighbours (see Complexity/Logics/Propositional/Parity/DepthThree.lean).

Main definitions

• Cslib.BitString.flipOn: flip the bits in a set of positions.
• Cslib.Logic.PL.ContainsSubcube: a set of words contains a subcube of a given dimension.
• Cslib.Logic.PL.isolatedDirections, Cslib.Logic.PL.ClauseSet.neighbors.

Main results

• Cslib.Logic.PL.ClauseSet.card_compl_isolatedDirections_le: few non-isolated directions.
• Cslib.Logic.PL.ClauseSet.card_solutions_le_of_neighbors: the bound in bounded degree.
• Cslib.Logic.PL.ClauseSet.card_solutions_le_of_not_containsSubcube: the bound.

References

• R. Paturi, P. Pudlák, F. Zane, Satisfiability coding lemma
• R. Impagliazzo, R. Paturi, F. Zane, Which problems have strongly exponential complexity?

def Cslib.Logic.PL.ContainsSubcube {N : ℕ} (S : Set (BitString N)) (d : ℕ) : Prop

The set S contains a subcube of dimension d: all the words obtained from one word by flipping bits in a fixed set of d positions.

theorem Cslib.Logic.PL.ContainsSubcube.mono {N : ℕ} {S T : Set (BitString N)} (hST : S ⊆ T) {d : ℕ} (h : ContainsSubcube S d) : ContainsSubcube T d

def Cslib.Logic.PL.isolatedDirections {N : ℕ} (S : Finset (BitString N)) (x : BitString N) : Finset (Fin N)

The isolated directions of x in S: the positions whose flip leaves S.

def Cslib.Logic.PL.ClauseSet.neighbors {N : ℕ} (ψ : ClauseSet (Fin N)) (u : Fin N) : Finset (Fin N)

The variables w ≠ u that share a clause of ψ with u: the neighbours of u in the co-occurrence graph.

def Cslib.Logic.PL.ClauseSet.Meets {N : ℕ} (C : Finset (Literal (Fin N))) (T : Finset (Fin N)) : Prop

The clause C mentions a variable of T.

theorem Cslib.Logic.PL.ClauseSet.flipOn_biUnion_mem_solutions_of_separated {N : ℕ} {ι : Type u_1} {ψ : ClauseSet (Fin N)} {x : BitString N} {s : Finset ι} {T : ι → Finset (Fin N)} (hx : x ∈ ψ.solutions) (hmove : ∀ j ∈ s, BitString.flipOn (T j) x ∈ ψ.solutions) (hsep : ∀ C ∈ ψ, ∀ j ∈ s, ∀ j' ∈ s, j ≠ j' → Meets C (T j) → ¬Meets C (T j')) {J : Finset ι} (hJ : J ⊆ s) : BitString.flipOn (J.biUnion T) x ∈ ψ.solutions

Separated moves combine: if the moves T j, j ∈ s, of a solution x are pairwise separated (no clause meets two of them), flipping the union of any of them keeps x a solution.

theorem Cslib.Logic.PL.ClauseSet.mem_neighbors_comm {N : ℕ} {ψ : ClauseSet (Fin N)} {u w : Fin N} : w ∈ ψ.neighbors u ↔ u ∈ ψ.neighbors w

theorem Cslib.Logic.PL.ClauseSet.card_compl_isolatedDirections_le {N : ℕ} {ψ : ClauseSet (Fin N)} {Δ D : ℕ} (hdeg : ∀ (u : Fin N), (ψ.neighbors u).card ≤ Δ) (hfree : ¬ContainsSubcube (↑ψ.solutions) D) {x : BitString N} (hx : x ∈ ψ.solutions) : (Finset.univ \ isolatedDirections ψ.solutions x).card ≤ (D - 1) * (Δ + 1)

Few non-isolated directions: if every variable has at most Δ neighbours and the solutions contain no subcube of dimension D, every solution has at most (D - 1)(Δ + 1) directions in which it is not isolated. A largest set of pairwise non-adjacent non-isolated directions spans a subcube of solutions, and its closed neighbourhood holds every non-isolated direction.

theorem Cslib.Logic.PL.ClauseSet.card_neighbors_le {N : ℕ} {ψ : ClauseSet (Fin N)} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) (u : Fin N) : (ψ.neighbors u).card ≤ ψ.occurrences u * (k - 1)

In a clause set of width at most k, a variable in c clauses has at most c (k - 1) neighbours.

theorem Cslib.Logic.PL.ClauseSet.card_solutions_le_of_neighbors {N : ℕ} {ψ : ClauseSet (Fin N)} {k Δ D : ℕ} (hk1 : 1 ≤ k) (hk : ∀ C ∈ ψ, C.card ≤ k) (hdeg : ∀ (u : Fin N), (ψ.neighbors u).card ≤ Δ) (hfree : ¬ContainsSubcube (↑ψ.solutions) D) : ↑ψ.solutions.card ≤ 2 ^ ((1 - 1 / ↑k) * ↑N + ↑((D - 1) * (Δ + 1)) / ↑k)

Few solutions in bounded degree: if every clause of ψ has at most k ≥ 1 literals, every variable has at most Δ neighbours, and the solutions contain no subcube of dimension D, then ψ has at most 2 ^ ((1 - 1 / k) N + (D - 1)(Δ + 1) / k) solutions.

theorem Cslib.Logic.PL.ClauseSet.card_solutions_le_of_not_containsSubcube (k : ℕ) (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ) (φ : ClauseSet (Fin N)) (D : ℕ), (∀ C ∈ φ, C.card ≤ k) → ¬ContainsSubcube (↑φ.solutions) D → ↑φ.solutions.card ≤ 2 ^ ((1 - 1 / ↑k + ε) * ↑N + C * ↑D)

Formulas without large subcubes of solutions have few solutions: for every width k ≥ 1 and every ε > 0 there is a constant C such that every clause set of width k over N variables whose solutions contain no subcube of dimension D has at most 2 ^ ((1 - 1 / k + ε) N + C D) solutions.

theorem Cslib.Logic.PL.CNF.card_filter_eval_le_of_not_containsSubcube (k : ℕ) (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ) (φ : CNF (Fin N)) (D : ℕ), (∀ c ∈ φ, List.length c ≤ k) → ¬ContainsSubcube {x : BitString N | eval x φ = true} D → ↑{x : BitString N | eval x φ = true}.card ≤ 2 ^ ((1 - 1 / ↑k + ε) * ↑N + C * ↑D)

Formulas without large subcubes of solutions have few solutions: for every width k ≥ 1 and every ε > 0 there is a constant C such that every formula in conjunctive normal form of width k over N variables whose solutions contain no subcube of dimension D has at most 2 ^ ((1 - 1 / k + ε) N + C D) solutions.