The complement of 2SAT in nondeterministic logarithmic space

A nondeterministic counter program (Cslib.Complexity.TwoSAT.decider) accepts, on the encoding of a formula φ, exactly when φ ∉ TwoSAT (Cslib.Complexity.TwoSAT.accepts_decider_iff). It first guesses which of two reasons to look for:

• a clause that is empty or has more than two literals: it guesses the clause and counts its literals;
• a variable x with a path from x to ¬x and one back in the implication graph (Cslib.Logic.PL.CNF.Implies) Papadimitriou, Theorem 16.3: it guesses an occurrence of x and walks from x, first to ¬x and then back to x, giving up after as many steps as the input has bits in each half.

These are all the reasons (Cslib.Complexity.notMem_TwoSAT_iff), by the theorem of Aspvall, Plass and Tarjan [APT79]. The walk stores its current literal as the position of an occurrence of its variable and a polarity. A step guesses a clause and one of its literals ℓ', checks that the clause has one or two literals and that its other literal, or ℓ' itself for a unit clause, is the negation of the current literal, which is the arc from the current literal to ℓ' of the implication graph, and moves to ℓ'. Variables are compared digit by digit through their positions (Cslib.Complexity.TwoSAT.cmpVarCode), so only positions, counters and flags are stored, all at most the length of the input. The strategy, guessing the two paths, is that of Papadimitriou, Theorem 16.3; the program, its register layout and the positional comparison of variables are this library's own.

Main definitions

• Cslib.Complexity.TwoSAT.decider: the nondeterministic counter program.

Main results

• Cslib.Complexity.TwoSAT.accepts_decider_iff: it accepts exactly the formulas outside TwoSAT.
• Cslib.Complexity.TwoSAT.exists_decidesInLogSpace_compl: one nondeterministic machine decides the complement of TwoSAT in logarithmic space, every branch halting.

References

• C. H. Papadimitriou, Computational Complexity, Theorem 16.3
• B. Aspvall, M. F. Plass, R. E. Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas

def Cslib.Complexity.TwoSAT.decider : Turing.CounterProgram

The decider of the complement of TwoSAT. Register 0 holds the choice, register 1 a scanning position, registers 2, 3 and 4 the occurrence of the starting variable, the occurrence of the current variable and the current polarity, registers 5, 6 and 7 the phase, the number of steps and the length of the input, registers 8 to 10 the literals of a guessed clause, registers 11 and 12 the next literal and the other one, and registers 13 to 15 cursors. Label 102 accepts and label 103 rejects.

theorem Cslib.Complexity.TwoSAT.length_code_decider : decider.code.length = 104

Registers

structure Cslib.Complexity.TwoSAT.St : Type

The registers other than the choice.

• p : ℕ

  Register 1.

• o₀ : ℕ

  Register 2.

• cur : ℕ

  Register 3.

• sgn : ℕ

  Register 4.

• phase : ℕ

  Register 5.

• steps : ℕ

  Register 6.

• len : ℕ

  Register 7.

• q₁ : ℕ

  Register 8.

• q₂ : ℕ

  Register 9.

• q₃ : ℕ

  Register 10.

• o₁ : ℕ

  Register 11.

• o₂ : ℕ

  Register 12.

• t₁ : ℕ

  Register 13.

• t₂ : ℕ

  Register 14.

• t : ℕ

  Register 15.

def Cslib.Complexity.TwoSAT.St.regs (st : St) (c : ℕ) : List ℕ

The registers, with the choice c.

def Cslib.Complexity.TwoSAT.St.Bounded (B : ℕ) (st : St) : Prop

All registers other than the choice are at most B.

theorem Cslib.Complexity.TwoSAT.St.forall_mem_regs {B : ℕ} {st : St} {c : ℕ} (h : Bounded B st) (hc : c ≤ B) (r : ℕ) : r ∈ st.regs c → r ≤ B

@[simp]

theorem Cslib.Complexity.TwoSAT.withChoice_regs (l : ℕ) (st : St) (c : ℕ) (b : Bool) : Turing.CounterProgram.withChoice (l, st.regs c) b = (l, st.regs b.toNat)

@[simp]

theorem Cslib.Complexity.TwoSAT.length_regs (st : St) (c : ℕ) : (st.regs c).length = 16

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_1 (st : St) (c : ℕ) : (st.regs c).getD 1 0 = st.p

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_1 (st : St) (c x : ℕ) : (st.regs c).set 1 x = { p := x, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_2 (st : St) (c : ℕ) : (st.regs c).getD 2 0 = st.o₀

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_2 (st : St) (c x : ℕ) : (st.regs c).set 2 x = { p := st.p, o₀ := x, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_3 (st : St) (c : ℕ) : (st.regs c).getD 3 0 = st.cur

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_3 (st : St) (c x : ℕ) : (st.regs c).set 3 x = { p := st.p, o₀ := st.o₀, cur := x, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_4 (st : St) (c : ℕ) : (st.regs c).getD 4 0 = st.sgn

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_4 (st : St) (c x : ℕ) : (st.regs c).set 4 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := x, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_5 (st : St) (c : ℕ) : (st.regs c).getD 5 0 = st.phase

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_5 (st : St) (c x : ℕ) : (st.regs c).set 5 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := x, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_6 (st : St) (c : ℕ) : (st.regs c).getD 6 0 = st.steps

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_6 (st : St) (c x : ℕ) : (st.regs c).set 6 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := x, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_7 (st : St) (c : ℕ) : (st.regs c).getD 7 0 = st.len

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_7 (st : St) (c x : ℕ) : (st.regs c).set 7 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := x, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_8 (st : St) (c : ℕ) : (st.regs c).getD 8 0 = st.q₁

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_8 (st : St) (c x : ℕ) : (st.regs c).set 8 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := x, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_9 (st : St) (c : ℕ) : (st.regs c).getD 9 0 = st.q₂

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_9 (st : St) (c x : ℕ) : (st.regs c).set 9 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := x, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_10 (st : St) (c : ℕ) : (st.regs c).getD 10 0 = st.q₃

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_10 (st : St) (c x : ℕ) : (st.regs c).set 10 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := x, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_11 (st : St) (c : ℕ) : (st.regs c).getD 11 0 = st.o₁

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_11 (st : St) (c x : ℕ) : (st.regs c).set 11 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := x, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_12 (st : St) (c : ℕ) : (st.regs c).getD 12 0 = st.o₂

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_12 (st : St) (c x : ℕ) : (st.regs c).set 12 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := x, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_13 (st : St) (c : ℕ) : (st.regs c).getD 13 0 = st.t₁

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_13 (st : St) (c x : ℕ) : (st.regs c).set 13 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := x, t₂ := st.t₂, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_14 (st : St) (c : ℕ) : (st.regs c).getD 14 0 = st.t₂

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_14 (st : St) (c x : ℕ) : (st.regs c).set 14 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := x, t := st.t }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_15 (st : St) (c : ℕ) : (st.regs c).getD 15 0 = st.t

@[simp]

theorem Cslib.Complexity.TwoSAT.St.set_regs_15 (st : St) (c x : ℕ) : (st.regs c).set 15 x = { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := x }.regs c

@[simp]

theorem Cslib.Complexity.TwoSAT.St.getD_regs_0 (st : St) (c : ℕ) : (st.regs c).getD 0 0 = c

Halting

theorem Cslib.Complexity.TwoSAT.reject_ne_accept : Turing.CounterProgram.Instr.reject ≠ Turing.CounterProgram.Instr.accept

def Cslib.Complexity.TwoSAT.Post (φ : Logic.PL.CNF ℕ) (s : Turing.CounterProgram.Config) : Prop

What every halt guarantees: accepting only formulas outside TwoSAT.

@[reducible, inline]

abbrev Cslib.Complexity.TwoSAT.bnd (φ : Logic.PL.CNF ℕ) : ℕ

The bound on the registers: the length of the input, plus one for the choice.

theorem Cslib.Complexity.TwoSAT.ab_reject {φ : Logic.PL.CNF ℕ} {Q : Turing.CounterProgram.Config → Prop} {st : St} (hB : St.Bounded (bnd φ) st) (b : Bool) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (103, st.regs b.toNat)

Every branch from the rejecting halt.

theorem Cslib.Complexity.TwoSAT.ab_accept {φ : Logic.PL.CNF ℕ} {Q : Turing.CounterProgram.Config → Prop} {st : St} (hB : St.Bounded (bnd φ) st) (b : Bool) (h : φ ∉ TwoSAT) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (102, st.regs b.toNat)

Every branch from the accepting halt, for a formula outside TwoSAT.

theorem Cslib.Complexity.TwoSAT.ab_step_reject {φ : Logic.PL.CNF ℕ} {Q : Turing.CounterProgram.Config → Prop} {l : ℕ} {st : St} (hB : St.Bounded (bnd φ) st) (hh : decider.halted (l, st.regs 0) = false) (b : Bool) (hstep : ∀ (b : Bool), decider.step (encCNF φ) (l, st.regs b.toNat) = (103, st.regs b.toNat)) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (l, st.regs b.toNat)

A step to the rejecting halt.

Code placement

theorem Cslib.Complexity.TwoSAT.codeAt_skipClause₅ : decider.CodeAt 5 (skipClauseCode 5 1 3)

theorem Cslib.Complexity.TwoSAT.codeAt_skipLit₁₂ : decider.CodeAt 12 (skipLitCode 12 8 15)

theorem Cslib.Complexity.TwoSAT.codeAt_skipLit₁₆ : decider.CodeAt 16 (skipLitCode 16 8 19)

A clause of width zero or more than two

theorem Cslib.Complexity.TwoSAT.le_bnd_of_infixAt {φ : Logic.PL.CNF ℕ} {p : ℕ} {u : List Bool} (h : InfixAt (encCNF φ) p u) (hu : u ≠ []) : p + u.length ≤ bnd φ

A position within the input is at most the bound.

theorem Cslib.Complexity.TwoSAT.literalBits_ne_nil (v : ℕ) (b : Bool) : literalBits v b ≠ []

theorem Cslib.Complexity.TwoSAT.reaches_width {φ : Logic.PL.CNF ℕ} {p : ℕ} {c : Logic.PL.Clause ℕ} (hc : LitsAt (encCNF φ) p c) {st : St} (hp : st.p = p) (hB : St.Bounded (bnd φ) st) (x : ℕ) (hx : x ≤ bnd φ) : ∃ (st' : St), St.Bounded (bnd φ) st' ∧ decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (10, st.regs x) (if List.length c = 0 ∨ 3 ≤ List.length c then 102 else 103, st'.regs x)

The width of a clause: from label 10, the run accepts exactly when the clause at the scanning position is empty or has more than two literals.

Every branch through the decider

theorem Cslib.Complexity.TwoSAT.ab_of_reaches {φ : Logic.PL.CNF ℕ} {Q : Turing.CounterProgram.Config → Prop} {l l' : ℕ} {st st' : St} {x : ℕ} (h : decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (l, st.regs x) (l', st'.regs x)) (hcont : ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (l', st'.regs b.toNat)) (b : Bool) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (l, st.regs b.toNat)

Every branch through deterministic code, then from its end.

theorem Cslib.Complexity.TwoSAT.ab_choice {φ : Logic.PL.CNF ℕ} {Q : Turing.CounterProgram.Config → Prop} {l yes no : ℕ} {st : St} (hl : decider.instr l = Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg 0) (Turing.CounterProgram.Expr.const 1) yes no) (hB : St.Bounded (bnd φ) st) (hyes : ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (yes, st.regs b.toNat)) (hno : ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (no, st.regs b.toNat)) (b : Bool) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) Q (l, st.regs b.toNat)

A step at a choice: yes for the choice 0 and no for the choice 1.

theorem Cslib.Complexity.TwoSAT.LitsAt.getElem?_isSome {w : List Bool} {p : ℕ} {c : Logic.PL.Clause ℕ} (h : LitsAt w p c) : ∃ (b : Bool), w[p]? = some b

The first bit of a clause is that of its first literal, or the end of the clause.

theorem Cslib.Complexity.TwoSAT.readLabel_some (yes no e : ℕ) {o : Option Bool} (h : ∃ (b : Bool), o = some b) (hyn : yes = no) : Turing.CounterProgram.readLabel yes no e o = yes

theorem Cslib.Complexity.TwoSAT.length_clauseBits (c : Logic.PL.Clause ℕ) : (clauseBits c).length = (List.flatMap (fun (l : Logic.PL.Literal ℕ) => literalBits l.1 l.2) c).length + 1

The length of the bits of a clause.

theorem Cslib.Complexity.TwoSAT.ab_modeA {φ : Logic.PL.CNF ℕ} (cs : Logic.PL.CNF ℕ) {p : ℕ} {st : St} : (∀ c ∈ cs, c ∈ φ) → ClausesAt (encCNF φ) p cs → st.p = p → St.Bounded (bnd φ) st → ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (x : Turing.CounterProgram.Config) => False) (3, st.regs b.toNat)

Every branch looking for a clause of width zero or more than two, from the clauses cs, halts, accepting only when it finds one.

The walk

def Cslib.Complexity.TwoSAT.Occ (φ : Logic.PL.CNF ℕ) (pos v : ℕ) (b : Bool) : Prop

The position pos holds an occurrence of the literal (v, b) of the formula.

def Cslib.Complexity.TwoSAT.LoopInv (φ : Logic.PL.CNF ℕ) (st : St) : Prop

The registers at the head of the walk: the starting occurrence of a variable x, the occurrence of the variable v of the current literal and its polarity, the number of steps within the length of the input, and the paths found so far: from x to the current literal in the first phase, and from x to ¬x and from ¬x to the current literal in the second.

def Cslib.Complexity.TwoSAT.measure (φ : Logic.PL.CNF ℕ) (st : St) : ℕ

The measure of the walk: the steps left, the first phase counting double.

theorem Cslib.Complexity.TwoSAT.codeAt_skipClause₂₂ : decider.CodeAt 22 (skipClauseCode 22 1 20)

theorem Cslib.Complexity.TwoSAT.codeAt_skipLit₂₉ : decider.CodeAt 29 (skipLitCode 29 1 27)

theorem Cslib.Complexity.TwoSAT.reaches_pick {φ : Logic.PL.CNF ℕ} {p : ℕ} {st : St} (hp : st.p = p) (hB : St.Bounded (bnd φ) st) : decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (32, st.regs 0) (35, { p := st.p, o₀ := p, cur := p, sgn := 1, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs 0)

The chosen occurrence becomes the starting one and the current one, with polarity 1.

theorem Cslib.Complexity.TwoSAT.ab_startLit {φ : Logic.PL.CNF ℕ} {c : Logic.PL.Clause ℕ} (hcφ : c ∈ φ) (ls : Logic.PL.Clause ℕ) {p : ℕ} {st : St} : (∀ l ∈ ls, l ∈ c) → LitsAt (encCNF φ) p ls → st.p = p → St.Bounded (bnd φ) st → st.phase = 0 → st.steps = 0 → st.len = (encCNF φ).length → ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (s : Turing.CounterProgram.Config) => ∃ (st' : St) (b' : Bool), s = (35, st'.regs b'.toNat) ∧ LoopInv φ st') (27, st.regs b.toNat)

Every branch choosing the starting occurrence within a clause, from its literals ls, rejects or reaches the head of the walk.

theorem Cslib.Complexity.TwoSAT.ab_start {φ : Logic.PL.CNF ℕ} (cs : Logic.PL.CNF ℕ) {p : ℕ} {st : St} : (∀ c ∈ cs, c ∈ φ) → ClausesAt (encCNF φ) p cs → st.p = p → St.Bounded (bnd φ) st → st.phase = 0 → st.steps = 0 → st.len = (encCNF φ).length → ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (s : Turing.CounterProgram.Config) => ∃ (st' : St) (b' : Bool), s = (35, st'.regs b'.toNat) ∧ LoopInv φ st') (20, st.regs b.toNat)

Every branch choosing the starting occurrence, from the clauses cs, rejects or reaches the head of the walk.

theorem Cslib.Complexity.TwoSAT.codeAt_cmpVar₇₉ : decider.CodeAt 79 (cmpVarCode 79 12 3 13 14 89 103)

theorem Cslib.Complexity.TwoSAT.codeAt_sign₈₉ : decider.CodeAt 89 (signCode 89 12 15 93 94)

theorem Cslib.Complexity.TwoSAT.codeAt_sign₉₆ : decider.CodeAt 96 (signCode 96 11 15 100 101)

theorem Cslib.Complexity.TwoSAT.reaches_check {φ : Logic.PL.CNF ℕ} {st : St} {v : ℕ} {b₁ : Bool} (hcur : InfixAt (encCNF φ) st.cur (literalBits v b₁)) (hsgn : st.sgn ≤ 1) {ℓ' m : Logic.PL.Literal ℕ} (ho₁ : InfixAt (encCNF φ) st.o₁ (literalBits ℓ'.1 ℓ'.2)) (ho₂ : InfixAt (encCNF φ) st.o₂ (literalBits m.1 m.2)) (hB : St.Bounded (bnd φ) st) : ∃ (st' : St), St.Bounded (bnd φ) st' ∧ decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (79, st.regs 0) (if m = Std.Sat.Literal.negate (v, decide (st.sgn = 1)) then 35 else 103, st'.regs 0) ∧ (m = Std.Sat.Literal.negate (v, decide (st.sgn = 1)) → st'.o₀ = st.o₀ ∧ st'.phase = st.phase ∧ st'.steps = st.steps ∧ st'.len = st.len ∧ st'.cur = st.o₁ ∧ st'.sgn = ℓ'.2.toNat)

Checking an arc and moving along it, deterministically: from label 79, with the occurrences of literals ℓ' and m in registers 11 and 12, the run moves to ℓ' at the head of the walk when m is the negation of the current literal, and rejects otherwise.

theorem Cslib.Complexity.TwoSAT.ab_check {φ : Logic.PL.CNF ℕ} {st : St} {c : Logic.PL.Clause ℕ} (hcφ : c ∈ φ) {v : ℕ} {b₁ : Bool} (hcur : InfixAt (encCNF φ) st.cur (literalBits v b₁)) (hsgn : st.sgn ≤ 1) {ℓ' m : Logic.PL.Literal ℕ} (hℓ' : ℓ' ∈ c) (hm : m ∈ c) (hc : ∀ y ∈ c, y = m ∨ y = ℓ') (ho₁ : InfixAt (encCNF φ) st.o₁ (literalBits ℓ'.1 ℓ'.2)) (ho₂ : InfixAt (encCNF φ) st.o₂ (literalBits m.1 m.2)) (hB : St.Bounded (bnd φ) st) (b : Bool) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (s : Turing.CounterProgram.Config) => ∃ (st' : St) (b' : Bool), s = (35, st'.regs b'.toNat) ∧ st'.o₀ = st.o₀ ∧ st'.phase = st.phase ∧ st'.steps = st.steps ∧ st'.len = st.len ∧ st'.cur = st.o₁ ∧ st'.sgn = ℓ'.2.toNat ∧ St.Bounded (bnd φ) st' ∧ φ.Implies (v, decide (st.sgn = 1)) ℓ') (79, st.regs b.toNat)

Every branch checking an arc and moving along it: from label 79, with the occurrences of literals ℓ' and m of a clause c in registers 11 and 12, every branch rejects or moves to ℓ' when m is the negation of the current literal, in which case the arc exists.

theorem Cslib.Complexity.TwoSAT.codeAt_skipLit₆₃ : decider.CodeAt 63 (skipLitCode 63 9 66)

theorem Cslib.Complexity.TwoSAT.codeAt_skipLit₇₀ : decider.CodeAt 70 (skipLitCode 70 10 73)

theorem Cslib.Complexity.TwoSAT.codeAt_skipClause₅₅ : decider.CodeAt 55 (skipClauseCode 55 1 53)

def Cslib.Complexity.TwoSAT.Ready (φ : Logic.PL.CNF ℕ) (st st' : St) (c : Logic.PL.Clause ℕ) : Prop

The registers at label 79: the walk unchanged, and the occurrences of two literals ℓ' and m of the clause c in registers 11 and 12, such that c has no other literal.

def Cslib.Complexity.TwoSAT.Same (st st' : St) : Prop

The registers of the walk agree.

theorem Cslib.Complexity.TwoSAT.Same.rfl' {st : St} : Same st st

theorem Cslib.Complexity.TwoSAT.reaches_inspect {φ : Logic.PL.CNF ℕ} {q : ℕ} {c : Logic.PL.Clause ℕ} (hc : LitsAt (encCNF φ) q c) {st : St} (hp : st.p = q) (hB : St.Bounded (bnd φ) st) : ∃ (st' : St), St.Bounded (bnd φ) st' ∧ Same st st' ∧ ((c = [] ∨ 3 ≤ List.length c) ∧ decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (60, st.regs 0) (103, st'.regs 0) ∨ (∃ (m₁ : Logic.PL.Literal ℕ), c = [m₁] ∧ InfixAt (encCNF φ) st'.o₁ (literalBits m₁.1 m₁.2) ∧ InfixAt (encCNF φ) st'.o₂ (literalBits m₁.1 m₁.2) ∧ decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (60, st.regs 0) (79, st'.regs 0)) ∨ ∃ (m₁ : Logic.PL.Literal ℕ) (m₂ : Logic.PL.Literal ℕ), c = [m₁, m₂] ∧ InfixAt (encCNF φ) st'.q₁ (literalBits m₁.1 m₁.2) ∧ InfixAt (encCNF φ) st'.q₂ (literalBits m₂.1 m₂.2) ∧ decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (60, st.regs 0) (74, st'.regs 0))

Reading a guessed clause, deterministically, up to the guess of its literal ℓ': an empty clause or one with more than two literals is rejected, the literal of a unit clause is taken, and the two literals of a clause of width two are placed in registers 8 and 9.

def Cslib.Complexity.TwoSAT.pairSt (st : St) (first : Bool) : St

The registers after the guess of ℓ' in a clause of width two.

theorem Cslib.Complexity.TwoSAT.reaches_pair {φ : Logic.PL.CNF ℕ} {st : St} (hB : St.Bounded (bnd φ) st) (first : Bool) : decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (if first = true then 75 else 77, st.regs 0) (79, (pairSt st first).regs 0)

The guess of ℓ' in a clause of width two: the first literal, or the second.

theorem Cslib.Complexity.TwoSAT.ab_inspect {φ : Logic.PL.CNF ℕ} {p : ℕ} {c : Logic.PL.Clause ℕ} (hc : LitsAt (encCNF φ) p c) {st : St} (hp : st.p = p) (hB : St.Bounded (bnd φ) st) (b : Bool) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (s : Turing.CounterProgram.Config) => ∃ (st' : St) (b' : Bool), s = (79, st'.regs b'.toNat) ∧ Ready φ st st' c) (60, st.regs b.toNat)

Every branch reading a guessed clause rejects it when it is empty or has more than two literals, and otherwise guesses its literal ℓ', the other literal being m.

theorem Cslib.Complexity.TwoSAT.ab_scan {φ : Logic.PL.CNF ℕ} (cs : Logic.PL.CNF ℕ) {p : ℕ} {st : St} : (∀ c ∈ cs, c ∈ φ) → ClausesAt (encCNF φ) p cs → st.p = p → St.Bounded (bnd φ) st → ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (s : Turing.CounterProgram.Config) => ∃ (st' : St) (b' : Bool), ∃ c ∈ φ, s = (79, st'.regs b'.toNat) ∧ Ready φ st st' c) (53, st.regs b.toNat)

Every branch guessing a clause, from the clauses cs, rejects or reaches label 79 ready to check one of them.

theorem Cslib.Complexity.TwoSAT.decide_toNat_eq_one (b : Bool) : decide (b.toNat = 1) = b

def Cslib.Complexity.TwoSAT.stepSt (st : St) : St

The registers after the test of the number of steps.

theorem Cslib.Complexity.TwoSAT.reaches_steps {φ : Logic.PL.CNF ℕ} {st : St} (hB : St.Bounded (bnd φ) st) (hlen : st.len = (encCNF φ).length) (hs : st.steps < st.len) : decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (50, st.regs 0) (53, (stepSt st).regs 0)

The test of the number of steps, deterministically: from label 50, the run continues to guess a clause when fewer steps than the length of the input were taken.

theorem Cslib.Complexity.TwoSAT.stepSt_bounded {φ : Logic.PL.CNF ℕ} {st : St} (hB : St.Bounded (bnd φ) st) (hlen : st.len = (encCNF φ).length) (hs : st.steps < st.len) : St.Bounded (bnd φ) (stepSt st)

theorem Cslib.Complexity.TwoSAT.ab_walk {φ : Logic.PL.CNF ℕ} {st : St} (hinv : LoopInv φ st) (b : Bool) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (s : Turing.CounterProgram.Config) => ∃ (st' : St) (b' : Bool), s = (35, st'.regs b'.toNat) ∧ LoopInv φ st' ∧ measure φ st' < measure φ st) (50, st.regs b.toNat)

Every branch of a step of the walk: from label 50, every branch rejects or comes back to the head of the walk one step further along an arc.

theorem Cslib.Complexity.TwoSAT.codeAt_cmpVar₃₅ : decider.CodeAt 35 (cmpVarCode 35 3 2 13 14 45 50)

theorem Cslib.Complexity.TwoSAT.LoopInv.cursors {φ : Logic.PL.CNF ℕ} {st : St} (h : LoopInv φ st) {x y : ℕ} (hx : x ≤ bnd φ) (hy : y ≤ bnd φ) : LoopInv φ { p := st.p, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := x, t₂ := y, t := st.t }

The invariant does not depend on the cursors.

def Cslib.Complexity.TwoSAT.headOut (st : St) (same : Prop) [Decidable same] (X Y : ℕ) : ℕ × St

Where the head of the walk goes: when the current literal is the end of the half, the walk switches to the second half, or accepts at the end of the second; otherwise it continues.

theorem Cslib.Complexity.TwoSAT.reaches_head {φ : Logic.PL.CNF ℕ} {st : St} {x v : ℕ} {b₀ b₁ : Bool} (hO₀ : InfixAt (encCNF φ) st.o₀ (literalBits x b₀)) (hOc : InfixAt (encCNF φ) st.cur (literalBits v b₁)) (hsgn : st.sgn ≤ 1) (hph : st.phase ≤ 1) (hB : St.Bounded (bnd φ) st) : ∃ (X : ℕ) (Y : ℕ), X ≤ bnd φ ∧ Y ≤ bnd φ ∧ decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (35, st.regs 0) ((headOut st (v = x) X Y).1, (headOut st (v = x) X Y).2.regs 0)

The head of the walk, deterministically: it compares the current variable v with the starting variable x, and the polarity with the phase.

theorem Cslib.Complexity.TwoSAT.ab_head {φ : Logic.PL.CNF ℕ} {st : St} (hinv : LoopInv φ st) (b : Bool) : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (s : Turing.CounterProgram.Config) => ∃ (st' : St) (b' : Bool), s = (35, st'.regs b'.toNat) ∧ LoopInv φ st' ∧ measure φ st' < measure φ st) (35, st.regs b.toNat)

Every branch from the head of the walk halts, accepting only when both paths are found, or comes back to it with a smaller measure.

theorem Cslib.Complexity.TwoSAT.ab_loop {φ : Logic.PL.CNF ℕ} (n : ℕ) (st : St) : measure φ st = n → LoopInv φ st → ∀ (b : Bool), decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (x : Turing.CounterProgram.Config) => False) (35, st.regs b.toNat)

Every branch from the head of the walk halts, accepting only when both paths are found.

Every branch from the start

theorem Cslib.Complexity.TwoSAT.reaches_count {φ : Logic.PL.CNF ℕ} (j : ℕ) : j ≤ (encCNF φ).length → decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (0, { len := j }.regs 0) (2, { len := (encCNF φ).length }.regs 0)

The input is counted into register 7.

theorem Cslib.Complexity.TwoSAT.init_decider : decider.init = (0, { }.regs 0)

theorem Cslib.Complexity.TwoSAT.allBranches_decider {φ : Logic.PL.CNF ℕ} : decider.AllBranches (encCNF φ) (bnd φ) (Post φ) (fun (x : Turing.CounterProgram.Config) => False) decider.init

Every branch of the decider halts, accepting only formulas outside TwoSAT, with registers at most the length of the input plus one.

An accepting branch

theorem Cslib.Complexity.TwoSAT.branches_of_reaches' {φ : Logic.PL.CNF ℕ} {l l' : ℕ} {st st' : St} {x : ℕ} (h : decider.Reaches (encCNF φ) (decider.Oblivious (bnd φ)) (l, st.regs x) (l', st'.regs x)) (hne : l ≠ l') (b b' : Bool) : Turing.CounterProgram.Branches (l, st.regs b.toNat) (l', st'.regs b'.toNat)

One branch through deterministic code, with any choices before and after.

theorem Cslib.Complexity.TwoSAT.branches_choice {φ : Logic.PL.CNF ℕ} {l yes no : ℕ} (hl : decider.instr l = Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg 0) (Turing.CounterProgram.Expr.const 1) yes no) (st : St) (b b' : Bool) : Turing.CounterProgram.Branches (l, st.regs b.toNat) (if b = true then no else yes, st.regs b'.toNat)

One step at a choice, taking the choice b.

theorem Cslib.Complexity.TwoSAT.branches_scan {φ : Logic.PL.CNF ℕ} {l₀ skip inspect : ℕ} (h₀ : decider.instr l₀ = Turing.CounterProgram.Instr.read (Turing.CounterProgram.Expr.reg 1) (l₀ + 1) (l₀ + 1) 103) (h₁ : decider.instr (l₀ + 1) = Turing.CounterProgram.Instr.lt (Turing.CounterProgram.Expr.reg 0) (Turing.CounterProgram.Expr.const 1) inspect skip) (hskip : decider.CodeAt skip (skipClauseCode skip 1 l₀)) (hne : l₀ ≠ l₀ + 1) (hsk : skip ≠ l₀) (cs : Logic.PL.CNF ℕ) {p : ℕ} {st : St} : ClausesAt (encCNF φ) p cs → st.p = p → St.Bounded (bnd φ) st → ∀ (i : ℕ) (hi : i < List.length cs) (b b' : Bool), ∃ (q : ℕ), LitsAt (encCNF φ) q cs[i] ∧ q ≤ bnd φ ∧ Turing.CounterProgram.Branches (l₀, st.regs b.toNat) (inspect, { p := q, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs b'.toNat)

A branch guessing a clause of a scanning loop: the code at l₀ reads the scanning position, the choice at l₀ + 1 inspects the clause at inspect or skips it with the code at skip.

theorem Cslib.Complexity.TwoSAT.branches_lit {φ : Logic.PL.CNF ℕ} (ls : Logic.PL.Clause ℕ) {p : ℕ} {st : St} : LitsAt (encCNF φ) p ls → st.p = p → St.Bounded (bnd φ) st → ∀ (j : ℕ) (hj : j < List.length ls) (b b' : Bool), ∃ (q : ℕ), InfixAt (encCNF φ) q (literalBits ls[j].1 ls[j].2) ∧ Turing.CounterProgram.Branches (27, st.regs b.toNat) (32, { p := q, o₀ := st.o₀, cur := st.cur, sgn := st.sgn, phase := st.phase, steps := st.steps, len := st.len, q₁ := st.q₁, q₂ := st.q₂, q₃ := st.q₃, o₁ := st.o₁, o₂ := st.o₂, t₁ := st.t₁, t₂ := st.t₂, t := st.t }.regs b'.toNat)

A branch guessing a literal of a clause, at label 27.

theorem Cslib.Complexity.TwoSAT.branches_modeA {φ : Logic.PL.CNF ℕ} {c : Logic.PL.Clause ℕ} (hc : c ∈ φ) (hw : List.length c = 0 ∨ 3 ≤ List.length c) : ∃ (s : Turing.CounterProgram.Config), Turing.CounterProgram.Branches decider.init s ∧ decider.instr s.1 = Turing.CounterProgram.Instr.accept

An accepting branch for a clause of width zero or more than two.

theorem Cslib.Complexity.TwoSAT.branches_arc {φ : Logic.PL.CNF ℕ} {st : St} {v : ℕ} {b₁ : Bool} (hcur : InfixAt (encCNF φ) st.cur (literalBits v b₁)) (hsgn : st.sgn ≤ 1) (hB : St.Bounded (bnd φ) st) (hlen : st.len = (encCNF φ).length) (hs : st.steps < st.len) (hw : ∀ c ∈ φ, 1 ≤ List.length c ∧ List.length c ≤ 2) {ℓ' : Logic.PL.Literal ℕ} (harc : φ.Implies (v, decide (st.sgn = 1)) ℓ') (b : Bool) : ∃ (st' : St) (b' : Bool), Turing.CounterProgram.Branches (50, st.regs b.toNat) (35, st'.regs b'.toNat) ∧ st'.o₀ = st.o₀ ∧ st'.phase = st.phase ∧ st'.steps = st.steps + 1 ∧ st'.len = st.len ∧ Occ φ st'.cur ℓ'.1 ℓ'.2 ∧ st'.sgn = ℓ'.2.toNat ∧ St.Bounded (bnd φ) st'

A branch along an arc of the implication graph, from label 50 back to the head of the walk, for a formula whose clauses have one or two literals.

theorem Cslib.Complexity.TwoSAT.length_flatten_le_length_encCNF (φ : Logic.PL.CNF ℕ) : (List.flatten φ).length ≤ (encCNF φ).length

A formula has at most as many occurrences of literals as its encoding has bits.

theorem Cslib.Complexity.TwoSAT.branches_modeB {φ : Logic.PL.CNF ℕ} (hw : ∀ c ∈ φ, 1 ≤ List.length c ∧ List.length c ≤ 2) {x : ℕ} (h₁ : Relation.ReflTransGen φ.Implies (x, true) (x, false)) (h₂ : Relation.ReflTransGen φ.Implies (x, false) (x, true)) : ∃ (s : Turing.CounterProgram.Config), Turing.CounterProgram.Branches decider.init s ∧ decider.instr s.1 = Turing.CounterProgram.Instr.accept

An accepting branch for a variable x with a path from x to ¬x and one back, for a formula whose clauses have one or two literals.

theorem Cslib.Complexity.TwoSAT.accepts_decider_iff {φ : Logic.PL.CNF ℕ} : (∃ (s : Turing.CounterProgram.Config), Turing.CounterProgram.Branches decider.init s ∧ decider.instr s.1 = Turing.CounterProgram.Instr.accept) ↔ φ ∉ TwoSAT

The decider accepts exactly the formulas outside TwoSAT: some branch accepts exactly then.

theorem Cslib.Complexity.TwoSAT.exists_decidesInLogSpace_compl : ∃ (k : ℕ) (State : Type) (_ : Finite State) (ntm : Turing.MultiTapeNTM k Bool State) (c : ℕ), ntm.DecidesInSpace encCNF TwoSATᶜ fun (φ : Logic.PL.CNF ℕ) => c * ((encCNF φ).length.log2 + 1)

The complement of TwoSAT is decided in nondeterministic logarithmic space: one nondeterministic machine decides it within space logarithmic in the length of the encoding, every branch halting.