k-CNFs without large subcubes have few solutions

A move of a solution x of a clause set ψ is a nonempty set T of variables with x ⊕ e_T again a solution; two moves are separated when no clause meets both. Separated moves combine freely (Lemma 3), so in a clause set whose co-occurrence graph has maximum degree Δ and whose solutions contain no subcube of dimension D, every solution has at most (D - 1)(Δ + 1) non-isolated directions (Lemma 4). The satisfiability coding lemma (Complexitylib.Circuits.KCNF.Coding) then bounds the number of solutions. After sparsification (Complexitylib.Circuits.KCNF.Sparsification) every k-CNF is a union of at most 2 ^ (ε N) such pieces, which gives Theorem A: a k-CNF whose solutions contain no subcube of dimension D has at most 2 ^ ((1 - 1/k + ε) N + C D) solutions.

The exponent 1 - 1/k cannot be improved, already for D = 1: the k-CNF requiring even parity on each of N/k disjoint blocks of k variables has 2 ^ ((1 - 1/k) N) solutions, no two of which are neighbours (this example is not formalized here).

Main results

• flipOn_mem_solutions_of_closed (Lemma 3 (a)): the part of a move that no clause connects to the rest of the move is a move.
• flipOn_biUnion_mem_solutions_of_separated (Lemma 3 (b)): every union of pairwise separated moves is a move.
• card_compl_isolatedDirections_le (Lemma 4): local far-isolation, d = 1.
• card_neighbors_le_occurrences_mul: a variable occurring in c clauses of width k has at most c (k - 1) neighbours.
• card_solutions_le_of_neighbors (Theorem A, bounded degree): a clause set of width k ≥ 1 and co-occurrence degree Δ whose solutions contain no subcube of dimension D has at most 2 ^ ((1 - 1/k) N + (D - 1)(Δ + 1)/k) solutions.
• card_solutions_le_of_not_containsSubcube, CNF.card_accepting_le_of_not_containsSubcube (Theorem A): for every k ≥ 1 and ε > 0 there is C such that every k-CNF whose solutions contain no subcube of dimension D has at most 2 ^ ((1 - 1/k + ε) N + C D) solutions.

theorem Complexity.ClauseSet.flipOn_mem_solutions_of_closed {N : ℕ} {ψ : ClauseSet N} {x : BitString N} {T T' : Finset (Fin N)} (hx : x ∈ ψ.solutions) (hT : x.flipOn T ∈ ψ.solutions) (hsub : T' ⊆ T) (hclosed : ∀ C ∈ ψ, (∃ l ∈ C, l.var ∈ T') → ¬∃ l ∈ C, l.var ∈ T \ T') : x.flipOn T' ∈ ψ.solutions

Lemma 3 (a). If x and x ⊕ e_T are solutions, T' ⊆ T, and no clause mentions both a variable of T' and a variable of T \ T', then x ⊕ e_{T'} is a solution. In particular every connected component of a move in the co-occurrence graph is a move.

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

Lemma 3 (b). Let x be a solution and T j, for j ∈ s, moves of x that are pairwise separated: no clause mentions variables of two of them. Then for every J ⊆ s, x ⊕ e_{⋃_{j ∈ J} T j} is a solution.

theorem Complexity.ClauseSet.card_compl_isolatedDirections_le {N : ℕ} {ψ : ClauseSet 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)

Lemma 4 (local far-isolation, d = 1). If every variable has at most Δ neighbours in the co-occurrence graph of ψ and the solutions of ψ contain no subcube of dimension D, then every solution x has at most (D - 1)(Δ + 1) directions i with x ⊕ e_i a solution.

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

In a clause set whose clauses have at most k literals, a variable mentioned by c clauses has at most c (k - 1) neighbours in the co-occurrence graph.

theorem Complexity.ClauseSet.card_solutions_le_of_neighbors {N : ℕ} {ψ : ClauseSet 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)

Theorem A for bounded co-occurrence degree. Let every clause of ψ have at most k ≥ 1 literals, let every variable have at most Δ neighbours in the co-occurrence graph, and let the solutions of ψ contain no subcube of dimension D. Then |sol ψ| ≤ 2 ^ ((1 - 1/k) N + (D - 1)(Δ + 1)/k).

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

Theorem A. For every k ≥ 1 and ε > 0 there is a constant C ≥ 0 such that every clause set φ over N variables whose clauses have at most k literals, and whose solutions contain no subcube of dimension D, has at most 2 ^ ((1 - 1/k + ε) N + C D) solutions.

theorem Complexity.CNF.card_accepting_le_of_not_containsSubcube (k : ℕ) (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ) (φ : CNF N) (D : ℕ), φ.width ≤ k → ¬ContainsSubcube {x : BitString N | φ.eval x = true} D → ↑{x : BitString N | φ.eval x = true}.card ≤ 2 ^ ((1 - 1 / ↑k + ε) * ↑N + C * ↑D)

Theorem A for CNFs. For every k ≥ 1 and ε > 0 there is a constant C ≥ 0 such that every CNF φ of width at most k over N variables whose accepted inputs contain no subcube of dimension D accepts at most 2 ^ ((1 - 1/k + ε) N + C D) inputs.