The strong exponential time hypothesis implies the orthogonal vectors hypothesis

The split-and-list reduction of Williams [Wil05] (Cslib.Complexity.toOV) splits the n distinct variables of a formula with m clauses into halves of ⌊n / 2⌋ and ⌈n / 2⌉ variables. To each assignment of a half it assigns the vector of length m whose coordinate j is true when no literal of clause j on a variable of the half is satisfied (Cslib.Complexity.OV.clauseVector). Two such vectors, one for each half, are orthogonal exactly when every clause is satisfied by one of the two partial assignments, that is when together they satisfy the formula. So the formula is satisfiable exactly when the instance toOV φ, of 2 ^ ⌊n / 2⌋ and 2 ^ ⌈n / 2⌉ vectors of dimension m, is in OV (Cslib.Complexity.toOV_mem_OV_iff).

The reduction writes its output of about 2 ^ ⌈n / 2⌉ m bits within time 2 ^ ⌈n / 2⌉ times a polynomial in the length of the encoded formula (Cslib.Complexity.exists_computableInO_toOV). The vectors are streamed to the output one at a time (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.iterate_unary_stream_sum); accumulating them in a list would cost time quadratic in the number of vectors. Then a decider for OV within time N ^ (2 - ε) times a polynomial in the dimension, on N vectors, decides SAT within time 2 ^ ((1 - ε / 2) n) times a polynomial, for 0 < ε ≤ 1 (Cslib.Complexity.DecidableInTimeO.decidableInExpTime_SAT), and the strong exponential time hypothesis implies the orthogonal vectors hypothesis (Cslib.Complexity.OVH_of_SETH).

The orthogonal vectors hypothesis is stated with a polynomial factor in the dimension. Its form for dimension c log N, which follows from the strong exponential time hypothesis with the sparsification lemma, is not proved here.

Main definitions

• Cslib.Complexity.OV.clauseVector, Cslib.Complexity.OV.halfVectors: the vectors of the assignments of a half of the variables.
• Cslib.Complexity.toOV: the split-and-list reduction.

Main results

• Cslib.Complexity.toOV_mem_OV_iff: toOV φ ∈ OV ↔ φ ∈ SAT.
• Cslib.Complexity.exists_computableInO_toOV: the reduction runs within time 2 ^ ⌈n / 2⌉ times a polynomial.
• Cslib.Complexity.DecidableInTimeO.decidableInExpTime_SAT: a fast OV decider gives a fast SAT decider.
• Cslib.Complexity.OVH_of_SETH: SETH → OVH.

References

• R. Williams, A new algorithm for optimal 2-constraint satisfaction and its implications

Orthogonality

theorem Cslib.Complexity.OV.orthogonal_map_map {γ : Type u_1} {l : List γ} {f g : γ → Bool} : Orthogonal (List.map f l) (List.map g l) ↔ ∀ x ∈ l, f x = false ∨ g x = false

Vectors indexed by the same list are orthogonal when no index is true in both.

The split-and-list reduction

def Cslib.Complexity.OV.satisfiesOn (vs : List ℕ) (i : ℕ) (c : Logic.PL.Clause ℕ) : Bool

Whether the assignment numbered by i on the variables vs satisfies a literal of the clause c on a variable of vs.

def Cslib.Complexity.OV.clauseVector (φ : Logic.PL.CNF ℕ) (vs : List ℕ) (i : ℕ) : List Bool

The vector of the assignment numbered by i on the variables vs: coordinate j is true when the assignment satisfies no literal of clause j of φ on a variable of vs.

def Cslib.Complexity.OV.halfVectors (φ : Logic.PL.CNF ℕ) (vs : List ℕ) : List (List Bool)

The vectors of the 2 ^ |vs| assignments numbered on the variables vs.

def Cslib.Complexity.OV.firstVars (φ : Logic.PL.CNF ℕ) : List ℕ

The first ⌊n / 2⌋ of the n distinct variables.

def Cslib.Complexity.OV.secondVars (φ : Logic.PL.CNF ℕ) : List ℕ

The last ⌈n / 2⌉ of the n distinct variables.

def Cslib.Complexity.toOV (φ : Logic.PL.CNF ℕ) : List (List Bool) × List (List Bool)

The split-and-list reduction [Wil05]: the vectors of the assignments of the first ⌊n / 2⌋ and of the last ⌈n / 2⌉ of the n distinct variables of a formula.

theorem Cslib.Complexity.OV.satisfiesOn_eq_true_iff {vs : List ℕ} {i : ℕ} {c : Logic.PL.Clause ℕ} : satisfiesOn vs i c = true ↔ ∃ l ∈ c, l.1 ∈ vs ∧ Logic.PL.bitsAssignment vs i l.1 = l.2

theorem Cslib.Complexity.OV.length_firstVars (φ : Logic.PL.CNF ℕ) : (firstVars φ).length = φ.numVars / 2

theorem Cslib.Complexity.OV.length_secondVars (φ : Logic.PL.CNF ℕ) : (secondVars φ).length = φ.numVars - φ.numVars / 2

theorem Cslib.Complexity.OV.length_halfVectors (φ : Logic.PL.CNF ℕ) (vs : List ℕ) : (halfVectors φ vs).length = 2 ^ vs.length

theorem Cslib.Complexity.OV.length_of_mem_halfVectors {φ : Logic.PL.CNF ℕ} {vs : List ℕ} {v : List Bool} (hv : v ∈ halfVectors φ vs) : v.length = List.length φ

theorem Cslib.Complexity.OV.orthogonal_clauseVector_iff {φ : Logic.PL.CNF ℕ} {vs₁ vs₂ : List ℕ} (hdisj : vs₁.Disjoint vs₂) (hcover : ∀ v ∈ φ.vars, v ∈ vs₁ ∨ v ∈ vs₂) (i₁ i₂ : ℕ) : Orthogonal (clauseVector φ vs₁ i₁) (clauseVector φ vs₂ i₂) ↔ Logic.PL.CNF.eval (fun (v : ℕ) => if v ∈ vs₁ then Logic.PL.bitsAssignment vs₁ i₁ v else Logic.PL.bitsAssignment vs₂ i₂ v) φ = true

Orthogonal vectors are satisfying assignments. For disjoint lists of variables vs₁ and vs₂ covering the variables of φ, the vectors of the assignments numbered by i₁ on vs₁ and by i₂ on vs₂ are orthogonal exactly when the two assignments together satisfy φ.

theorem Cslib.Complexity.toOV_mem_OV_iff (φ : Logic.PL.CNF ℕ) : toOV φ ∈ OV ↔ φ ∈ SAT

The split-and-list reduction is correct [Wil05]: toOV φ ∈ OV ↔ φ ∈ SAT.

Sizes

theorem Cslib.Complexity.length_toOV_fst (φ : Logic.PL.CNF ℕ) : (toOV φ).1.length = 2 ^ (φ.numVars / 2)

theorem Cslib.Complexity.length_toOV_snd (φ : Logic.PL.CNF ℕ) : (toOV φ).2.length = 2 ^ (φ.numVars - φ.numVars / 2)

theorem Cslib.Complexity.OV.dim_le {p : List (List Bool) × List (List Bool)} {b : ℕ} (h : ∀ v ∈ p.1 ++ p.2, v.length ≤ b) : dim p ≤ b

The dimension is at most a bound on the lengths of all vectors.

theorem Cslib.Complexity.OV.dim_toOV_le (φ : Logic.PL.CNF ℕ) : dim (toOV φ) ≤ List.length φ

The vectors of toOV φ have one coordinate for each clause.

Running time

@[reducible, inline]

abbrev Cslib.Complexity.OV.StreamState : Type

The states of the stream of vectors: a formula, a list of variables, and the number of the next assignment.

@[reducible, inline]

abbrev Cslib.Complexity.OV.encStreamState : StreamState ↪ List Bool

Stream states encoded as framed tuples.

theorem Cslib.Complexity.OV.computableInPolyTime_clauseVector : Turing.MultiTapeTM.ComputableInPolyTime (fun (s : StreamState) => clauseVector s.1.1 s.1.2 s.2) encStreamState Turing.MultiTapeTM.encBits

Computing the vector of a numbered assignment is polynomial-time.

theorem Cslib.Complexity.OV.exists_computableInO_stream {half : Logic.PL.CNF ℕ → List ℕ} (hhalf : Turing.MultiTapeTM.ComputableInPolyTime half encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hlen : ∀ (φ : Logic.PL.CNF ℕ), (half φ).length ≤ (encCNF φ).length) {wrap : List Bool → List Bool} (hwrap : Turing.MultiTapeTM.ComputableInPolyTime wrap Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (fin : List Bool) : ∃ (e : ℕ), Turing.MultiTapeTM.ComputableInO (fun (φ : Logic.PL.CNF ℕ) => (List.map wrap (halfVectors φ (half φ))).flatten ++ fin) encCNF Turing.MultiTapeTM.encBits (fun (φ : Logic.PL.CNF ℕ) => 2 ^ (half φ).length * ((encCNF φ).length + 1) ^ e) fun (φ : Logic.PL.CNF ℕ) => 2 ^ (half φ).length * ((encCNF φ).length + 1) ^ e

Streaming the vectors of a half of the variables: the vectors of the 2 ^ |half φ| assignments numbered on half φ, each wrapped by wrap, followed by fin, are written within time 2 ^ |half φ| times a polynomial in the length of the encoded formula.

theorem Cslib.Complexity.OV.computableInPolyTime_firstVars : Turing.MultiTapeTM.ComputableInPolyTime firstVars encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.OV.computableInPolyTime_secondVars : Turing.MultiTapeTM.ComputableInPolyTime secondVars encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.Complexity.OV.length_firstVars_le (φ : Logic.PL.CNF ℕ) : (firstVars φ).length ≤ (encCNF φ).length

theorem Cslib.Complexity.OV.length_secondVars_le (φ : Logic.PL.CNF ℕ) : (secondVars φ).length ≤ (encCNF φ).length

theorem Cslib.Complexity.exists_computableInO_toOV : ∃ (e : ℕ), Turing.MultiTapeTM.ComputableInO toOV encCNF encOV (fun (φ : Logic.PL.CNF ℕ) => 2 ^ (φ.numVars - φ.numVars / 2) * ((encCNF φ).length + 1) ^ e) fun (φ : Logic.PL.CNF ℕ) => 2 ^ (φ.numVars - φ.numVars / 2) * ((encCNF φ).length + 1) ^ e

The split-and-list reduction is fast: it writes its output within time 2 ^ ⌈n / 2⌉ times a polynomial in the length of the encoded formula, on formulas with n variables.

Williams' theorem

theorem Cslib.Complexity.DecidableInTimeO.decidableInExpTime_SAT {ε : ℝ} (hε : 0 < ε) {e : ℕ} (h : DecidableInTimeO OV encOV fun (p : List (List Bool) × List (List Bool)) => ↑(p.1.length + p.2.length) ^ (2 - ε) * (↑(OV.dim p) + 1) ^ e) : DecidableInExpTime SAT encCNF Logic.PL.CNF.numVars (1 - min ε 1 / 2)

Williams' theorem [Wil05]: a decider for OV within time N ^ (2 - ε) times a polynomial in the dimension, on instances of N vectors, gives a decider for SAT within time 2 ^ ((1 - ε / 2) n) times a polynomial in the length of the encoded formula, on formulas with n variables, for 0 < ε ≤ 1; for ε > 1 it gives the exponent 1 / 2 of the reduction.

theorem Cslib.Complexity.OVH_of_SETH (h : SETH) : OVH

The strong exponential time hypothesis implies the orthogonal vectors hypothesis [Wil05].