The layout of encoded formulas

A formula is encoded (Cslib.Complexity.encCNF) by three levels of framed lists: the clauses, their literals, and the binary digits of each variable followed by the polarity. Unfolding the frames gives a flat layout (Cslib.Complexity.TwoSAT.encCNF_eq_flatMap): each clause is the bits of its literals followed by false, and a literal (v, b) is a group of eight bits for each binary digit d of v, seven markers true followed by d, then the ten bits [true, true, true, false, true, true, true, b, true, false] (Cslib.Complexity.TwoSAT.literalBits). A machine reading the encoding by position can thus tell a literal from the end of its clause by the first bit, a digit from the end of the variable by the fourth bit of a group, and read the digit or the polarity from the eighth.

The positions are handled with Cslib.Complexity.TwoSAT.InfixAt w p u, which says that the word u occurs in w at position p.

Main definitions

• Cslib.Complexity.TwoSAT.literalBits, Cslib.Complexity.TwoSAT.clauseBits: the flat layout.
• Cslib.Complexity.TwoSAT.InfixAt: a word occurring at a position.
• Cslib.Complexity.TwoSAT.clauseStart: the position of a clause.

Main results

• Cslib.Complexity.TwoSAT.encCNF_eq_flatMap: the flat layout of an encoded formula.
• Cslib.Complexity.TwoSAT.InfixAt.literal_digit, .literal_end, .clause_literal, .clause_end, Cslib.Complexity.TwoSAT.infixAt_clauseStart: reading the layout by position.

def Cslib.Complexity.TwoSAT.literalBits (v : ℕ) (b : Bool) : List Bool

The bits of a literal (v, b) in an encoded formula: the binary digits of v, each after seven markers, then the end of the digits, the polarity and the end of the literal.

def Cslib.Complexity.TwoSAT.clauseBits (c : Logic.PL.Clause ℕ) : List Bool

The bits of a clause in an encoded formula: its literals, then false.

@[simp]

theorem Cslib.Complexity.TwoSAT.length_literalBits (v : ℕ) (b : Bool) : (literalBits v b).length = 8 * v.bits.length + 10

theorem Cslib.Complexity.TwoSAT.frame_encClause (c : Logic.PL.Clause ℕ) : Turing.MultiTapeTM.frame ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)) c) = clauseBits c

The frame of a clause is its bits.

theorem Cslib.Complexity.TwoSAT.encCNF_eq_flatMap (φ : Logic.PL.CNF ℕ) : encCNF φ = List.flatMap clauseBits φ

The flat layout of an encoded formula.

Positions

def Cslib.Complexity.TwoSAT.InfixAt (w : List Bool) (p : ℕ) (u : List Bool) : Prop

The word u occurs in w at the position p.

theorem Cslib.Complexity.TwoSAT.InfixAt.append {w u v : List Bool} {p : ℕ} : InfixAt w p (u ++ v) ↔ InfixAt w p u ∧ InfixAt w (p + u.length) v

theorem Cslib.Complexity.TwoSAT.InfixAt.flatMap {w : List Bool} {p : ℕ} {α : Type u_1} {L : List α} {f : α → List Bool} (h : InfixAt w p (List.flatMap f L)) {i : ℕ} (hi : i < L.length) : InfixAt w (p + (List.map (fun (a : α) => (f a).length) (List.take i L)).sum) (f L[i])

The word of an element of a list, in the concatenation of the words of the elements.

theorem Cslib.Complexity.TwoSAT.InfixAt.getElem? {w u : List Bool} {p : ℕ} (h : InfixAt w p u) {q : ℕ} (hq : q < u.length) : w[p + q]? = u[q]?

The bit at an offset.

theorem Cslib.Complexity.TwoSAT.InfixAt.literal_digit {w : List Bool} {p v : ℕ} {b : Bool} (h : InfixAt w p (literalBits v b)) {k : ℕ} (hk : k < v.bits.length) : w[p + 8 * k]? = some true ∧ w[p + 8 * k + 3]? = some true ∧ w[p + 8 * k + 7]? = some v.bits[k]

A digit of a literal: the group of the digit k of v starts at 8 * k, its fourth bit is a marker and its eighth bit is the digit.

theorem Cslib.Complexity.TwoSAT.InfixAt.literal_end {w : List Bool} {p v : ℕ} {b : Bool} (h : InfixAt w p (literalBits v b)) : w[p + 8 * v.bits.length]? = some true ∧ w[p + 8 * v.bits.length + 3]? = some false ∧ w[p + 8 * v.bits.length + 7]? = some b

The end of a literal: after the groups of the digits, the fourth bit is false and the eighth bit is the polarity; the literal ends ten bits after the digits.

theorem Cslib.Complexity.TwoSAT.InfixAt.clause_literal {w : List Bool} {p : ℕ} {c : Logic.PL.Clause ℕ} (h : InfixAt w p (clauseBits c)) {j : ℕ} (hj : j < List.length c) : InfixAt w (p + (List.map (fun (l : Logic.PL.Literal ℕ) => (literalBits l.1 l.2).length) (List.take j c)).sum) (literalBits c[j].1 c[j].2)

A literal of a clause, at the offset of the literals before it.

theorem Cslib.Complexity.TwoSAT.InfixAt.clause_end {w : List Bool} {p : ℕ} {c : Logic.PL.Clause ℕ} (h : InfixAt w p (clauseBits c)) : w[p + (List.map (fun (l : Logic.PL.Literal ℕ) => (literalBits l.1 l.2).length) c).sum]? = some false

The end of a clause: false after all its literals.

def Cslib.Complexity.TwoSAT.clauseStart (φ : Logic.PL.CNF ℕ) (i : ℕ) : ℕ

The position of the clause i in an encoded formula.

theorem Cslib.Complexity.TwoSAT.infixAt_clauseStart (φ : Logic.PL.CNF ℕ) {i : ℕ} (hi : i < List.length φ) : InfixAt (encCNF φ) (clauseStart φ i) (clauseBits φ[i])

The clauses of an encoded formula, at their positions.

theorem Cslib.Complexity.TwoSAT.getElem?_clauseStart_length (φ : Logic.PL.CNF ℕ) : (encCNF φ)[clauseStart φ (List.length φ)]? = none

The encoding ends after the last clause.

theorem Cslib.Complexity.TwoSAT.clauseStart_succ (φ : Logic.PL.CNF ℕ) {i : ℕ} (hi : i < List.length φ) : clauseStart φ (i + 1) = clauseStart φ i + (clauseBits φ[i]).length

The clause i + 1 starts after the clause i.

theorem Cslib.Complexity.TwoSAT.InfixAt.le_length {w u : List Bool} {p : ℕ} (h : InfixAt w p u) (hu : u ≠ []) : p + u.length ≤ w.length

A nonempty word occurring in w ends within w.

theorem Cslib.Complexity.TwoSAT.InfixAt.literal_start {w : List Bool} {p v : ℕ} {b : Bool} (h : InfixAt w p (literalBits v b)) : w[p]? = some true

A literal starts with a marker.

def Cslib.Complexity.TwoSAT.LitsAt (w : List Bool) (p : ℕ) (ls : Logic.PL.Clause ℕ) : Prop

The literals ls occur at the position p, followed by the end of their clause.

theorem Cslib.Complexity.TwoSAT.LitsAt.getElem?_nil {w : List Bool} {p : ℕ} (h : LitsAt w p []) : w[p]? = some false

The end of a clause is false.

theorem Cslib.Complexity.TwoSAT.LitsAt.cons {w : List Bool} {p : ℕ} {l : Logic.PL.Literal ℕ} {ls : Logic.PL.Clause ℕ} (h : LitsAt w p (l :: ls)) : InfixAt w p (literalBits l.1 l.2) ∧ LitsAt w (p + (literalBits l.1 l.2).length) ls

A literal, then the rest of the clause.

theorem Cslib.Complexity.TwoSAT.LitsAt.le_length {w : List Bool} {p : ℕ} {ls : Logic.PL.Clause ℕ} (h : LitsAt w p ls) : p + (List.flatMap (fun (l : Logic.PL.Literal ℕ) => literalBits l.1 l.2) ls).length + 1 ≤ w.length

A clause ends within the word.

def Cslib.Complexity.TwoSAT.ClausesAt (w : List Bool) (p : ℕ) (cs : Logic.PL.CNF ℕ) : Prop

The clauses cs occur at the position p, up to the end of the word.

theorem Cslib.Complexity.TwoSAT.ClausesAt.getElem?_nil {w : List Bool} {p : ℕ} (h : ClausesAt w p []) : w[p]? = none

The word ends after the clauses.

theorem Cslib.Complexity.TwoSAT.ClausesAt.cons {w : List Bool} {p : ℕ} {c : Logic.PL.Clause ℕ} {cs : Logic.PL.CNF ℕ} (h : ClausesAt w p (c :: cs)) : LitsAt w p c ∧ ClausesAt w (p + (clauseBits c).length) cs

A clause, then the rest.

theorem Cslib.Complexity.TwoSAT.clausesAt_encCNF (φ : Logic.PL.CNF ℕ) : ClausesAt (encCNF φ) 0 φ

The clauses of an encoded formula occur from its start.

theorem Cslib.Complexity.TwoSAT.set_getD_self {regs : List ℕ} {i : ℕ} (hi : i < regs.length) : regs.set i (regs.getD i 0) = regs

Overwriting a register with its own value changes nothing.