Routines reading an encoded formula

Counter-program routines that navigate the flat layout of an encoded formula (Cslib.Complexity.TwoSAT.literalBits, Cslib.Complexity.TwoSAT.clauseBits) with positions held in registers, each placed at a label and continuing at given labels:

• Cslib.Complexity.TwoSAT.skipLitCode moves a position past a literal, group by group;
• Cslib.Complexity.TwoSAT.skipClauseCode moves a position past a clause, literal by literal;
• Cslib.Complexity.TwoSAT.cmpVarCode compares the variables of two literals digit by digit;
• Cslib.Complexity.TwoSAT.signCode reads the polarity of a literal.

None of them reads register 0, so they can be part of nondeterministic counter programs. Their specifications are deterministic runs (Turing.CounterProgram.Reaches) through configurations with bounded registers at instructions that do not read the choice (Turing.CounterProgram.Oblivious).

Main definitions

• Cslib.Complexity.TwoSAT.skipLitCode, Cslib.Complexity.TwoSAT.skipClauseCode, Cslib.Complexity.TwoSAT.cmpVarCode, Cslib.Complexity.TwoSAT.signCode.

Main results

• Cslib.Complexity.TwoSAT.reaches_skipLitCode, Cslib.Complexity.TwoSAT.reaches_skipClauseCode, Cslib.Complexity.TwoSAT.reaches_cmpVarCode, Cslib.Complexity.TwoSAT.reaches_signCode: their runs.

Skipping a literal

def Cslib.Complexity.TwoSAT.skipLitCode (b p exit : ℕ) : List Turing.CounterProgram.Instr

The code moving the position in register p past the literal there: groups with a marker as fourth bit are digits, eight bits long, and the end group is ten bits long.

theorem Cslib.Complexity.TwoSAT.reaches_skipLitCode {P : Turing.CounterProgram} {w : List Bool} {B b p exit : ℕ} (hcode : P.CodeAt b (skipLitCode b p exit)) (hp : p ≠ 0) {regs : List ℕ} (hlen : p < regs.length) {pos v : ℕ} {sgn : Bool} (hlit : InfixAt w pos (literalBits v sgn)) (hpos : regs.getD p 0 = pos) (hB : ∀ r ∈ regs, r ≤ B) (hend : pos + (literalBits v sgn).length ≤ B) : P.Reaches w (P.Oblivious B) (b, regs) (exit, regs.set p (pos + (literalBits v sgn).length))

Skipping a literal.

Skipping a clause

def Cslib.Complexity.TwoSAT.skipClauseCode (b p exit : ℕ) : List Turing.CounterProgram.Instr

The code moving the position in register p past the clause there, literal by literal.

theorem Cslib.Complexity.TwoSAT.reaches_skipClauseCode {P : Turing.CounterProgram} {w : List Bool} {B b p exit : ℕ} (hcode : P.CodeAt b (skipClauseCode b p exit)) (hp : p ≠ 0) {regs : List ℕ} (hlen : p < regs.length) {pos : ℕ} {ls : Logic.PL.Clause ℕ} (hls : LitsAt w pos ls) (hpos : regs.getD p 0 = pos) (hB : ∀ r ∈ regs, r ≤ B) (hend : pos + (List.flatMap (fun (l : Logic.PL.Literal ℕ) => literalBits l.1 l.2) ls).length + 1 ≤ B) : P.Reaches w (P.Oblivious B) (b, regs) (exit, regs.set p (pos + (List.flatMap (fun (l : Logic.PL.Literal ℕ) => literalBits l.1 l.2) ls).length + 1))

Skipping a clause.

Comparing variables

def Cslib.Complexity.TwoSAT.cmpVarCode (b p₁ p₂ t₁ t₂ eq ne : ℕ) : List Turing.CounterProgram.Instr

The code comparing the variables of the literals at the positions in registers p₁ and p₂, digit by digit, with cursors in registers t₁ and t₂: it continues at eq when they are the same variable and at ne otherwise.

theorem Cslib.Complexity.TwoSAT.reaches_cmpVarCode {P : Turing.CounterProgram} {w : List Bool} {B b p₁ p₂ t₁ t₂ eq ne : ℕ} (hcode : P.CodeAt b (cmpVarCode b p₁ p₂ t₁ t₂ eq ne)) (hp₁ : p₁ ≠ 0) (hp₂ : p₂ ≠ 0) (ht₁ : t₁ ≠ 0) (ht₂ : t₂ ≠ 0) (htt : t₁ ≠ t₂) (ht₁p₂ : t₁ ≠ p₂) {regs : List ℕ} (hlen₁ : t₁ < regs.length) (hlen₂ : t₂ < regs.length) {pos₁ pos₂ v₁ v₂ : ℕ} {s₁ s₂ : Bool} (hl₁ : InfixAt w pos₁ (literalBits v₁ s₁)) (hl₂ : InfixAt w pos₂ (literalBits v₂ s₂)) (hpos₁ : regs.getD p₁ 0 = pos₁) (hpos₂ : regs.getD p₂ 0 = pos₂) (hB : ∀ r ∈ regs, r ≤ B) (hend₁ : pos₁ + (literalBits v₁ s₁).length ≤ B) (hend₂ : pos₂ + (literalBits v₂ s₂).length ≤ B) : ∃ (x : ℕ) (y : ℕ), x ≤ B ∧ y ≤ B ∧ P.Reaches w (P.Oblivious B) (b, regs) (if v₁ = v₂ then eq else ne, (regs.set t₁ x).set t₂ y)

Comparing variables: the run ends at eq exactly when the variables are equal, with the cursors within the literals.

Reading the polarity

def Cslib.Complexity.TwoSAT.signCode (b p t yes no : ℕ) : List Turing.CounterProgram.Instr

The code reading the polarity of the literal at the position in register p, with a cursor in register t: it continues at yes for a positive literal and at no otherwise.

theorem Cslib.Complexity.TwoSAT.reaches_signCode {P : Turing.CounterProgram} {w : List Bool} {B b p t yes no : ℕ} (hcode : P.CodeAt b (signCode b p t yes no)) (hp : p ≠ 0) (ht : t ≠ 0) {regs : List ℕ} (hlen : t < regs.length) {pos v : ℕ} {sgn : Bool} (hlit : InfixAt w pos (literalBits v sgn)) (hpos : regs.getD p 0 = pos) (hB : ∀ r ∈ regs, r ≤ B) (hend : pos + (literalBits v sgn).length ≤ B) : P.Reaches w (P.Oblivious B) (b, regs) (if sgn = true then yes else no, regs.set t (pos + 8 * v.bits.length))

Reading the polarity.