Clause sets -- basic API

Evaluation of literals, flips x ⊕ e_T and the points agreeing with x off a set, membership in solution sets and forced sets, and the translation of a CNF to its clause set.

Main results

• BitString.card_filter_agree: exactly 2 ^ |F| points agree with x off F.
• CNF.sat_toClauseSet_iff: a CNF and its clause set have the same solutions.
• CNF.card_le_width_of_mem_toClauseSet: the clause set of a CNF has no wider clause.

theorem Complexity.Literal.eval_eq_true_iff {N : ℕ} (l : Literal N) (x : BitString N) : l.eval x = true ↔ x l.var = l.polarity

A literal is true exactly when its variable carries its polarity.

theorem Complexity.Literal.eq_of_eval_eq_true {N : ℕ} {l l' : Literal N} {x : BitString N} (hvar : l.var = l'.var) (h : l.eval x = true) (h' : l'.eval x = true) : l = l'

Two literals on the same variable that are both true under x are equal.

@[simp]

theorem Complexity.BitString.flipOn_apply {N : ℕ} (x : BitString N) (T : Finset (Fin N)) (i : Fin N) : x.flipOn T i = if i ∈ T then !x i else x i

theorem Complexity.BitString.flipOn_apply_of_mem {N : ℕ} {x : BitString N} {T : Finset (Fin N)} {i : Fin N} (h : i ∈ T) : x.flipOn T i = !x i

theorem Complexity.BitString.flipOn_apply_of_not_mem {N : ℕ} {x : BitString N} {T : Finset (Fin N)} {i : Fin N} (h : i ∉ T) : x.flipOn T i = x i

@[simp]

theorem Complexity.BitString.flipOn_empty {N : ℕ} (x : BitString N) : x.flipOn ∅ = x

Flipping nothing is the identity.

theorem Complexity.BitString.flipOn_apply_eq_of_iff {N : ℕ} {x : BitString N} {T U : Finset (Fin N)} {i : Fin N} (h : i ∈ T ↔ i ∈ U) : x.flipOn T i = x.flipOn U i

Two flips agree at every coordinate that lies in both sets or in neither.

@[simp]

theorem Complexity.BitString.flipOn_flipOn {N : ℕ} (x : BitString N) (T : Finset (Fin N)) : (x.flipOn T).flipOn T = x

Flipping twice is the identity.

theorem Complexity.BitString.flipOn_comm {N : ℕ} (x : BitString N) (T U : Finset (Fin N)) : (x.flipOn T).flipOn U = (x.flipOn U).flipOn T

Flips commute.

theorem Complexity.BitString.flipOn_injective {N : ℕ} (x : BitString N) : Function.Injective x.flipOn

x ↦ x ⊕ e_T is injective in T.

theorem Complexity.BitString.filter_agree_eq_image {N : ℕ} (x : BitString N) (F : Finset (Fin N)) : {y : BitString N | ∀ v ∉ F, y v = x v} = Finset.image x.flipOn F.powerset

The points that agree with x off F are exactly the points x ⊕ e_T with T ⊆ F.

theorem Complexity.BitString.card_filter_agree {N : ℕ} (x : BitString N) (F : Finset (Fin N)) : {y : BitString N | ∀ v ∉ F, y v = x v}.card = 2 ^ F.card

Exactly 2 ^ |F| points agree with x off F.

theorem Complexity.ClauseSet.mem_solutions {N : ℕ} {ψ : ClauseSet N} {x : BitString N} : x ∈ ψ.solutions ↔ ψ.Sat x

theorem Complexity.ClauseSet.mem_forced {N : ℕ} {ψ : ClauseSet N} {σ : Equiv.Perm (Fin N)} {x : BitString N} {v : Fin N} : v ∈ ψ.forced σ x ↔ ∃ C ∈ ψ, ∃ l ∈ C, l.var = v ∧ ∀ l' ∈ C, l' ≠ l → σ l'.var < σ v ∧ l'.eval x = false

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

A subcube of a set is a subcube of every larger set.

theorem Complexity.CNF.sat_toClauseSet_iff {N : ℕ} (φ : CNF N) (x : BitString N) : φ.toClauseSet.Sat x ↔ φ.eval x = true

A CNF and its clause set have the same solutions.

theorem Complexity.CNF.card_le_width_of_mem_toClauseSet {N : ℕ} {φ : CNF N} {C : Finset (Literal N)} (hC : C ∈ φ.toClauseSet) : C.card ≤ φ.width

A clause of the clause set of a CNF is no longer than the CNF's width.

theorem Complexity.CNF.mem_solutions_toClauseSet {N : ℕ} (φ : CNF N) (x : BitString N) : x ∈ φ.toClauseSet.solutions ↔ φ.eval x = true

The solutions of the clause set of a CNF are the inputs the CNF accepts.

theorem Complexity.CNF.solutions_toClauseSet {N : ℕ} (φ : CNF N) : φ.toClauseSet.solutions = {x : BitString N | φ.eval x = true}

The solutions of the clause set of a CNF, as a filter of the cube.

theorem Complexity.ClauseSet.eval_toCNF_eq_true_iff {N : ℕ} (ψ : ClauseSet N) (x : BitString N) : ψ.toCNF.eval x = true ↔ ψ.Sat x

The CNF of a clause set accepts exactly its solutions.

theorem Complexity.ClauseSet.width_toCNF_le {N : ℕ} {ψ : ClauseSet N} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) : ψ.toCNF.width ≤ k

The CNF of a clause set is no wider than its widest clause.

theorem Complexity.ClauseSet.occurrences_toCNF {N : ℕ} (ψ : ClauseSet N) (v : Fin N) : ψ.toCNF.occurrences v = ψ.occurrences v

The CNF of a clause set has as many clauses mentioning v as the clause set.