Sparsification on formulas

The branching step of the sparsification procedure on formulas in conjunctive normal form, as list operations: reduction (CNF.Sparsification.reduce), flowers and petals, the children (CNF.Sparsification.child) and a computed heavy-heart choice (CNF.Sparsification.choice).

Formulas are kept in a normal form (CNF.Sparsification.Normalized): no clause repeats a literal or has more than k literals, no two clauses have the same literals, and no clause strictly contains another. Then a formula and its clause set have the same number of clauses, and the list operations compute the clause-set operations of Cslib.Logic.PL.ClauseSet.Sparsification (CNF.Sparsification.toClauseSet_child). Any formula of width k is brought into normal form by CNF.Sparsification.normalize.

The candidate hearts of a clause C are its sublists selected by the subsets of the first k positions (CNF.Sparsification.hearts); for clauses of width k these are all of its subclauses, so every heavy heart is a candidate. The choice takes a heavy candidate of least rank c (k + 1) + (k - |H|), which has the smallest clause size c and then the largest heart: a valid choice (CNF.Sparsification.choice_spec). So the list-level step is a branching rule (CNF.Sparsification.rule) on the formulas in normal form, to which the analysis of the branching tree applies.

Main definitions

• Cslib.Logic.PL.CNF.Sparsification.subclause, Cslib.Logic.PL.CNF.Sparsification.reduce, Cslib.Logic.PL.CNF.Sparsification.flower, Cslib.Logic.PL.CNF.Sparsification.petals, Cslib.Logic.PL.CNF.Sparsification.intro, Cslib.Logic.PL.CNF.Sparsification.child, Cslib.Logic.PL.CNF.Sparsification.heavy, Cslib.Logic.PL.CNF.Sparsification.hearts, Cslib.Logic.PL.CNF.Sparsification.candidates, Cslib.Logic.PL.CNF.Sparsification.rank, Cslib.Logic.PL.CNF.Sparsification.choice, Cslib.Logic.PL.CNF.Sparsification.next: the list-level step.
• Cslib.Logic.PL.CNF.Sparsification.isSparse: the list-level test for sparseness.
• Cslib.Logic.PL.CNF.Sparsification.dedup, Cslib.Logic.PL.CNF.Sparsification.dedupClauses, Cslib.Logic.PL.CNF.Sparsification.normalize, Cslib.Logic.PL.CNF.Sparsification.Normalized: the normal form.
• Cslib.Logic.PL.CNF.Sparsification.rule: the list-level branching rule.

Main results

• Cslib.Logic.PL.CNF.Sparsification.toClauseSet_child: the list-level children compute the clause-set children.
• Cslib.Logic.PL.CNF.Sparsification.choice_spec: the computed choice is valid.
• Cslib.Logic.PL.CNF.Sparsification.isSparse_eq_true_iff: the list-level test decides sparseness.

References

• R. Impagliazzo, R. Paturi, F. Zane, Which problems have strongly exponential complexity?
• C. Calabro, R. Impagliazzo, R. Paturi, A duality between clause width and clause density for SAT

The list operations

def Cslib.Logic.PL.CNF.Sparsification.subclause {V : Type u_1} [DecidableEq V] (D C : Clause V) : Bool

Whether every literal of D is a literal of C.

def Cslib.Logic.PL.CNF.Sparsification.reduce {V : Type u_1} [DecidableEq V] (ψ : CNF V) : CNF V

Remove every clause whose literals strictly contain those of another clause.

def Cslib.Logic.PL.CNF.Sparsification.flower {V : Type u_1} [DecidableEq V] (ψ : CNF V) (c : ℕ) (H : Clause V) : CNF V

The flower of H at clause size c: the clauses of length c containing the literals of H.

def Cslib.Logic.PL.CNF.Sparsification.petals {V : Type u_1} [DecidableEq V] (ψ : CNF V) (c : ℕ) (H : Clause V) : CNF V

The petals C \ H of the flower of H.

def Cslib.Logic.PL.CNF.Sparsification.intro {V : Type u_1} [DecidableEq V] (ψ : CNF V) (c : ℕ) (H : Clause V) (b : Bool) : CNF V

The clauses a branch introduces: the heart (false) or the petals (true).

def Cslib.Logic.PL.CNF.Sparsification.child {V : Type u_1} [DecidableEq V] (ψ : CNF V) (c : ℕ) (H : Clause V) (b : Bool) : CNF V

A child of a branching node: add the introduced clauses and reduce.

def Cslib.Logic.PL.CNF.Sparsification.heavy {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : CNF V) (x : ℕ × Clause V) : Bool

Whether H is a heavy heart for clause size c, for the thresholds θ.

def Cslib.Logic.PL.CNF.Sparsification.hearts {V : Type u_1} (k : ℕ) (C : Clause V) : List (Clause V)

The candidate hearts of a clause: its sublists selected by subsets of the first k positions.

def Cslib.Logic.PL.CNF.Sparsification.candidates {V : Type u_1} (k : ℕ) (ψ : CNF V) : List (ℕ × Clause V)

The candidate pairs of a clause size and a heart: each clause with its candidate hearts.

def Cslib.Logic.PL.CNF.Sparsification.rank {V : Type u_1} (k : ℕ) (x : ℕ × Clause V) : ℕ

The rank c (k + 1) + (k - |H|) of a clause size c and a heart H: smaller sizes, and then larger hearts, have smaller ranks.

def Cslib.Logic.PL.CNF.Sparsification.choice {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (k : ℕ) (ψ : CNF V) : ℕ × Clause V

The computed choice: a heavy candidate of least rank, or (0, []) if there is none.

def Cslib.Logic.PL.CNF.Sparsification.isSparse {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (k : ℕ) (ψ : CNF V) : Bool

Whether no candidate is a heavy heart.

def Cslib.Logic.PL.CNF.Sparsification.next {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (k : ℕ) (ψ : CNF V) (b : Bool) : CNF V

One branching step: the heart (false) or petal (true) child for the computed choice.

def Cslib.Logic.PL.CNF.Sparsification.dedup {V : Type u_1} [DecidableEq V] (C : Clause V) : Clause V

Remove repeated literals of a clause, keeping first occurrences.

def Cslib.Logic.PL.CNF.Sparsification.dedupClauses {V : Type u_1} [DecidableEq V] (ψ : CNF V) : CNF V

Remove every clause with the same literals as an earlier clause.

def Cslib.Logic.PL.CNF.Sparsification.normalize {V : Type u_1} [DecidableEq V] (φ : CNF V) : CNF V

The normal form of a formula: repeated literals and clauses removed, and reduced.

Clause sets of formulas

theorem Cslib.Logic.PL.CNF.Sparsification.mem_toClauseSet {V : Type u_1} [DecidableEq V] {ψ : CNF V} {C : Finset (Literal V)} : C ∈ ψ.toClauseSet ↔ ∃ D ∈ ψ, List.toFinset D = C

A clause set C belongs to ψ.toClauseSet if and only if D.toFinset = C for some clause D ∈ ψ.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_append {V : Type u_1} [DecidableEq V] (ψ χ : CNF V) : (ψ ++ χ).toClauseSet = ψ.toClauseSet ∪ χ.toClauseSet

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_mono {V : Type u_1} [DecidableEq V] {ψ χ : CNF V} (h : ψ ⊆ χ) : ψ.toClauseSet ⊆ χ.toClauseSet

theorem Cslib.Logic.PL.CNF.Sparsification.subclause_eq_true_iff {V : Type u_1} [DecidableEq V] {D C : Clause V} : subclause D C = true ↔ List.toFinset D ⊆ List.toFinset C

theorem Cslib.Logic.PL.CNF.Sparsification.reduce_sublist {V : Type u_1} [DecidableEq V] (ψ : CNF V) : List.Sublist (reduce ψ) ψ

reduce ψ is a sublist of ψ.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_reduce {V : Type u_1} [DecidableEq V] (ψ : CNF V) : (reduce ψ).toClauseSet = ClauseSet.Sparsification.reduce ψ.toClauseSet

The list-level reduction computes the reduction of clause sets.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_flower {V : Type u_1} [DecidableEq V] {ψ : CNF V} (hnd : ∀ C ∈ ψ, List.Nodup C) (c : ℕ) (H : Clause V) : (flower ψ c H).toClauseSet = ClauseSet.Sparsification.flower ψ.toClauseSet c (List.toFinset H)

The list-level flower computes the clause-set flower when clauses have no repeated literals.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_petals {V : Type u_1} [DecidableEq V] {ψ : CNF V} (hnd : ∀ C ∈ ψ, List.Nodup C) (c : ℕ) (H : Clause V) : (petals ψ c H).toClauseSet = ClauseSet.Sparsification.petals ψ.toClauseSet c (List.toFinset H)

The list-level petals compute the clause-set petals when clauses have no repeated literals.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_child {V : Type u_1} [DecidableEq V] {ψ : CNF V} (hnd : ∀ C ∈ ψ, List.Nodup C) (c : ℕ) (H : Clause V) (b : Bool) : (child ψ c H b).toClauseSet = ClauseSet.Sparsification.child ψ.toClauseSet c (List.toFinset H) b

The list-level children compute the clause-set children.

The normal form

structure Cslib.Logic.PL.CNF.Sparsification.Normalized {V : Type u_1} [DecidableEq V] (k : ℕ) (ψ : CNF V) : Prop

The normal form of the list-level procedure, for width k: no clause repeats a literal or has more than k literals, no two clauses have the same literals, and no clause strictly contains another.

• nodup (C : Clause V) : C ∈ ψ → List.Nodup C
• length_le (C : Clause V) : C ∈ ψ → List.length C ≤ k
• nodup_toFinset : (List.map List.toFinset ψ).Nodup
• reduced : ClauseSet.Sparsification.Reduced ψ.toClauseSet

theorem Cslib.Logic.PL.CNF.Sparsification.Normalized.card_toClauseSet {V : Type u_1} [DecidableEq V] {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) : Finset.card ψ.toClauseSet = List.length ψ

A formula in normal form has as many clauses as its clause set.

theorem Cslib.Logic.PL.CNF.Sparsification.Normalized.card_le {V : Type u_1} [DecidableEq V] {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) (C : Finset (Literal V)) : C ∈ ψ.toClauseSet → C.card ≤ k

Every clause in the clause set of a k-normalized formula has at most k literals.

Candidates

theorem Cslib.Logic.PL.CNF.Sparsification.mem_hearts {V : Type u_1} {k : ℕ} {C H : Clause V} (hH : H ∈ hearts k C) : List.Sublist H C

Every candidate heart of C is a sublist of C.

theorem Cslib.Logic.PL.CNF.Sparsification.choice_spec {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) (hns : ¬ClauseSet.Sparsification.Sparse θ ψ.toClauseSet) : ClauseSet.Sparsification.Choice θ ψ.toClauseSet (choice θ k ψ).1 (List.toFinset (choice θ k ψ).2) ∧ List.Nodup (choice θ k ψ).2

The computed choice is valid. At a formula in normal form that is not sparse, the computed choice is a heavy heart with the smallest clause size, and among those the largest heart.

theorem Cslib.Logic.PL.CNF.Sparsification.isSparse_eq_true_iff {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) : isSparse θ k ψ = true ↔ ClauseSet.Sparsification.Sparse θ ψ.toClauseSet

The list-level test decides sparseness of formulas in normal form.

The step preserves the normal form

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_next {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) (b : Bool) : (next θ k ψ b).toClauseSet = ClauseSet.Sparsification.child ψ.toClauseSet (choice θ k ψ).1 (List.toFinset (choice θ k ψ).2) b

The clause set of next θ k ψ b equals the clause-set child for the computed choice.

theorem Cslib.Logic.PL.CNF.Sparsification.normalized_next {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) {k : ℕ} {ψ : CNF V} (h : Normalized k ψ) (hns : ¬ClauseSet.Sparsification.Sparse θ ψ.toClauseSet) (b : Bool) : Normalized k (next θ k ψ b)

At a non-sparse k-normalized formula, one branching step preserves normal form.

The branching rule

def Cslib.Logic.PL.CNF.Sparsification.rule {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ θ j) (k : ℕ) : ClauseSet.Sparsification.BranchingRule θ V { ψ : CNF V // Normalized k ψ }

The list-level branching rule, on formulas in normal form: the computed choice, and at a sparse formula no step.

Normalization

theorem Cslib.Logic.PL.CNF.Sparsification.toFinset_dedup {V : Type u_1} [DecidableEq V] (C : Clause V) : List.toFinset (dedup C) = List.toFinset C

Deduplicating a clause preserves its set of literals.

theorem Cslib.Logic.PL.CNF.Sparsification.dedupClauses_sublist {V : Type u_1} [DecidableEq V] (ψ : CNF V) : List.Sublist (dedupClauses ψ) ψ

dedupClauses ψ is a sublist of ψ.

theorem Cslib.Logic.PL.CNF.Sparsification.nodup_toFinset_dedupClauses {V : Type u_1} [DecidableEq V] (ψ : CNF V) : (List.map List.toFinset (dedupClauses ψ)).Nodup

Deduplicating clauses produces clauses with pairwise distinct literal sets.

theorem Cslib.Logic.PL.CNF.Sparsification.toClauseSet_dedupClauses {V : Type u_1} [DecidableEq V] (ψ : CNF V) : (dedupClauses ψ).toClauseSet = ψ.toClauseSet

Deduplicating clauses preserves the clause set.

theorem Cslib.Logic.PL.CNF.Sparsification.normalized_normalize {V : Type u_1} [DecidableEq V] {k : ℕ} {φ : CNF V} (hφ : ∀ C ∈ φ, List.length C ≤ k) : Normalized k (normalize φ)

Normalization. Every formula of width k has a normal form with the same solutions.

theorem Cslib.Logic.PL.CNF.Sparsification.sat_toClauseSet_normalize_iff {V : Type u_1} [DecidableEq V] (φ : CNF V) (x : V → Bool) : (normalize φ).toClauseSet.Sat x ↔ eval x φ = true

The clause set of normalize φ has the same solutions as φ.