Counting the clauses of an encoded formula

A formula's encoding is a stream of two-bit tokens, one of which marks the end of a clause. Counting those tokens counts the clauses, and an algorithm that has to loop over the clauses needs that count in unary.

The scan consumes two bits per step, so it is an iteration rather than a fold: the state is the count so far paired with the unread suffix.

Main definitions

• Complexity.sepCount — how many clause markers a bit string carries
• Complexity.ccStep — one two-bit step

Main results

• Complexity.ccStep_iterate — the scan counts
• Complexity.clauseCountFn_mem_FP, Complexity.clauseCountFn_eq — counting is polynomial time

def Complexity.sepCount : List Bool → ℕ

How many clause markers — the token 10 — a bit string carries.

Equations

• Complexity.sepCount (true :: false :: r) = Complexity.sepCount r + 1
• Complexity.sepCount (head :: head_1 :: r) = Complexity.sepCount r
• Complexity.sepCount x✝ = 0

@[simp]

theorem Complexity.sepCount_nil : sepCount [] = 0

theorem Complexity.sepCount_cons₂ (b0 b1 : Bool) (r : List Bool) : sepCount (b0 :: b1 :: r) = if b0 = true ∧ b1 = false then sepCount r + 1 else sepCount r

theorem Complexity.selectHead_cons (b : Bool) (t x y : List Bool) : Cobham.selectHead (b :: t) x y = if b = true then x else y

def Complexity.ccStep (z : List Bool) : List Bool

One step: read the next token, and count it if it marks a clause. The state is pair count unread.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.ccStep_mem_FP : ccStep ∈ FP

@[simp]

theorem Complexity.ccStep_nil (c : List Bool) : ccStep (pair c []) = pair c []

theorem Complexity.ccStep_cons₂ (c : List Bool) (b0 b1 : Bool) (r : List Bool) : ccStep (pair c (b0 :: b1 :: r)) = pair (if b0 = true ∧ b1 = false then true :: c else c) r

theorem Complexity.replicate_true_append_cons (n : ℕ) (c : List Bool) : List.replicate n true ++ true :: c = true :: (List.replicate n true ++ c)

theorem Complexity.ccStep_iterate (k : ℕ) (c s : List Bool) : s.length ≤ 2 * k → Even s.length → ccStep^[k] (pair c s) = pair (List.replicate (sepCount s) true ++ c) []

The scan counts.

The scan as one function

theorem Complexity.ccStep_one (c s : List Bool) : ∃ (X : List Bool) (Y : List Bool), ccStep (pair c s) = pair X Y ∧ X.length ≤ c.length + 1 ∧ Y.length ≤ s.length

theorem Complexity.ccStep_shape (k : ℕ) (c s : List Bool) : ∃ (c' : List Bool) (s' : List Bool), ccStep^[k] (pair c s) = pair c' s' ∧ c'.length ≤ c.length + k ∧ s'.length ≤ s.length

noncomputable def Complexity.clauseCountFn (z : List Bool) : List Bool

The clause count, in unary.

Equations

• Complexity.clauseCountFn z = Complexity.pairFst (Complexity.ccStep^[z.length] (Complexity.pair [] z))

theorem Complexity.clauseCountFn_mem_FP : clauseCountFn ∈ FP

theorem Complexity.clauseCountFn_eq {z : List Bool} (h : Even z.length) : clauseCountFn z = List.replicate (sepCount z) true