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).

Main results

• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_next: the step.
• Cslib.Logic.PL.CNF.Sparsification.computableInPolyTime_isSparse: the test for sparseness.
• 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_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_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.