Moves, local far-isolation, and the bounded-degree bound -- proofs

Internal proofs for Complexitylib.Circuits.KCNF.SubcubeFree.

A clause is satisfied by a point as soon as it is satisfied by a solution that agrees with the point on the clause's variables (sat_of_agree). Flipping a family of separated moves of a solution, or a part of a move that no clause connects to the rest, agrees on every clause with the solution or with one of the moved solutions. A largest set of pairwise non-adjacent non-isolated directions spans a subcube of solutions, so it has fewer than D elements when there is no subcube of dimension D; every non-isolated direction lies in its closed neighbourhood.

def Complexity.ClauseSet.Isolation.Meets {N : ℕ} (C : Finset (Literal N)) (T : Finset (Fin N)) : Prop

The clause C mentions a variable of T.

Equations

• Complexity.ClauseSet.Isolation.Meets C T = ∃ l ∈ C, l.var ∈ T

theorem Complexity.ClauseSet.Isolation.sat_of_agree {N : ℕ} {ψ : ClauseSet N} {w : BitString N} (h : ∀ C ∈ ψ, ∃ z ∈ ψ.solutions, ∀ l ∈ C, z l.var = w l.var) : w ∈ ψ.solutions

A point satisfies every clause of ψ that a solution agreeing with it on the clause's variables satisfies.

theorem Complexity.ClauseSet.Isolation.flipOn_mem_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 ∈ ψ, Meets C T' → ¬Meets C (T \ T')) : x.flipOn T' ∈ ψ.solutions

Lemma 3 (a). If x ⊕ e_T is a solution and no clause meets both T' ⊆ T and 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.Isolation.flipOn_biUnion_mem_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' → Meets C (T j) → ¬Meets C (T j')) {J : Finset ι} (hJ : J ⊆ s) : x.flipOn (J.biUnion T) ∈ ψ.solutions

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

theorem Complexity.ClauseSet.Isolation.flipOn_mem_of_independent {N : ℕ} {ψ : ClauseSet N} {x : BitString N} {M : Finset (Fin N)} (hx : x ∈ ψ.solutions) (hmove : ∀ i ∈ M, x.flipOn {i} ∈ ψ.solutions) (hind : ∀ u ∈ M, ∀ w ∈ M, u ≠ w → w ∉ ψ.neighbors u) {T : Finset (Fin N)} (hT : T ⊆ M) : x.flipOn T ∈ ψ.solutions

Pairwise non-adjacent singleton moves span a subcube of solutions.

theorem Complexity.ClauseSet.Isolation.mem_neighbors_comm {N : ℕ} {ψ : ClauseSet N} {u w : Fin N} : w ∈ ψ.neighbors u ↔ u ∈ ψ.neighbors w

theorem Complexity.ClauseSet.Isolation.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 contain no subcube of dimension D, then every solution has at most (D - 1)(Δ + 1) non-isolated directions.

theorem Complexity.ClauseSet.Isolation.card_neighbors_le {N : ℕ} {ψ : ClauseSet 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 mentioned by at most c clauses has at most c (k - 1) neighbours.

theorem Complexity.ClauseSet.Isolation.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)

The bounded-degree form of Theorem A. 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 contain no subcube of dimension D. Then |sol ψ| ≤ 2 ^ ((1 - 1/k) N + (D - 1)(Δ + 1)/k).