Sparsification -- the step is polynomial-time

The list-level sparsification step (Cslib.Logic.PL.CNF.Sparsification.next), the test for sparseness (Cslib.Logic.PL.CNF.Sparsification.isSparse) and normalization (Cslib.Logic.PL.CNF.Sparsification.normalize) are polynomial-time on the framed encoding of formulas, for any encoding of the variables. The width k is fixed, so a clause has a constant number of candidate hearts; the thresholds enter only through comparisons θ j ≤ n, which must themselves be polynomial-time in unary. They are for the explicit thresholds (Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_threshold_le).

The thresholds may also be read from a runtime parameter p, as θ p: the …With certificates take the parameter as part of the input and charge its encoding, so one machine serves every parameter value. The certificates for fixed thresholds are their specializations to a constant parameter.

Main results

• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_nextWith, Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_next: the step, for runtime and fixed thresholds.
• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparseWith, Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparse: the test for sparseness.
• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_heavyWith, Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_choiceWith: the heavy-heart test and the choice, for runtime thresholds.
• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_normalize: normalization.
• Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_threshold_le: comparisons with the explicit thresholds.

References

• R. Impagliazzo, R. Paturi, F. Zane, Which problems have strongly exponential complexity?

theorem Cslib.Logic.PL.ClauseSet.Sparsification.computableInPolyTime_threshold_le (k α : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (threshold k α p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool

Comparing the explicit thresholds with a number is polynomial-time in unary.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_reduce {V : Type} [DecidableEq V] (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime reduce (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The list-level reduction is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_dedupClauses {V : Type} [DecidableEq V] (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime dedupClauses (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

Removing duplicate clauses with identical literal sets is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_flower {V : Type} [DecidableEq V] (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : CNF V × ℕ × Clause V) => flower p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

Computing the flower of a clause size and heart is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_heavyWith {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {P : Type} {encP : P ↪ List Bool} {θ : P → ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × ℕ × ℕ) => decide (θ x.1 x.2.1 ≤ x.2.2)) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × CNF V × ℕ × Clause V) => heavy (θ x.1) x.2.1 x.2.2) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))))) Turing.MultiTapeTM.encBool

Testing a candidate against runtime thresholds. Testing whether a candidate (c, H) is heavy for thresholds θ p read from a runtime parameter p is polynomial-time, charging the encoding of p.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_const_threshold {θ : ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (θ p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : ℕ × ℕ × ℕ) => decide ((fun (x : ℕ) => θ) x.1 x.2.1 ≤ x.2.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool

A fixed threshold comparison, read through a constant runtime parameter. This specializes the …With certificates to fixed thresholds.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_heavy {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {θ : ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (θ p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : CNF V × ℕ × Clause V) => heavy θ p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))) Turing.MultiTapeTM.encBool

Testing whether a candidate (c, H) is heavy is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_candidates {V : Type} (encV : V ↪ List Bool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (candidates k) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))))

Listing the candidate pairs (c, H) of a formula is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_choiceWith {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {P : Type} {encP : P ↪ List Bool} {θ : P → ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × ℕ × ℕ) => decide (θ x.1 x.2.1 ≤ x.2.2)) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × CNF V) => choice (θ x.1) k x.2) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The choice for runtime thresholds is polynomial-time, charging the encoding of the parameter.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_choice {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {θ : ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (θ p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (choice θ k) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The computed choice is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparseWith {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {P : Type} {encP : P ↪ List Bool} {θ : P → ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × ℕ × ℕ) => decide (θ x.1 x.2.1 ≤ x.2.2)) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × CNF V) => isSparse (θ x.1) k x.2) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))) Turing.MultiTapeTM.encBool

The test for sparseness against runtime thresholds is polynomial-time, charging the encoding of the parameter.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparse {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {θ : ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (θ p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (isSparse θ k) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool

The list-level test for sparseness is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_nextWith {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {P : Type} {encP : P ↪ List Bool} {θ : P → ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × ℕ × ℕ) => decide (θ x.1 x.2.1 ≤ x.2.2)) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : P × CNF V × Bool) => next (θ x.1) k x.2.1 x.2.2) (Turing.MultiTapeTM.encPair encP (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The list-level step for runtime thresholds is polynomial-time, charging the encoding of the parameter.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_next {V : Type} [DecidableEq V] (encV : V ↪ List Bool) {θ : ℕ → ℕ} (hθ : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => decide (θ p.1 ≤ p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool) (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : CNF V × Bool) => next θ k p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

The list-level step is polynomial-time.

theorem Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_normalize {V : Type} [DecidableEq V] (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime normalize (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair encV Turing.MultiTapeTM.encBool)))

Normalization is polynomial-time.