Streaming specification for the CNF-to-3CNF transformation

This file gives a token-level specification of a machine-friendly Tseitin transducer. It reads the existing EncToken stream from left to right, keeps at most three decoded literals, and emits completed exact-width-three clauses as soon as a fourth source literal arrives. A literal body is represented only by its sign and a unary counter, matching the data a concrete TM can retain in finite control plus registers.

The formula-level entry point chooses the first fresh variable to be one more than the source bit length. This is deliberately easier for a TM to obtain than CNF.maxVar, and CNF.maxVar_le_encode_length ensures that the resulting variables are fresh. On a valid CNF.tokens stream, the emitted tokens and bits are exactly the encoding produced by CNF.to3Aux at that start value.

inductive Complexity.SAT.ThreeSAT.Streaming.Pending : Type

The source literals retained for the current clause. Three literals are enough: seeing a fourth emits one chain clause and rolls the window forward.

• zero : Pending
• one (a : Lit) : Pending
• two (a b : Lit) : Pending
• three (a b c : Lit) : Pending

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending : DecidableEq Pending

Equations

• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending = Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq

def Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (x✝ x✝¹ : Pending) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq Complexity.SAT.ThreeSAT.Streaming.Pending.zero Complexity.SAT.ThreeSAT.Streaming.Pending.zero = isTrue ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq Complexity.SAT.ThreeSAT.Streaming.Pending.zero (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq Complexity.SAT.ThreeSAT.Streaming.Pending.zero (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq Complexity.SAT.ThreeSAT.Streaming.Pending.zero (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) Complexity.SAT.ThreeSAT.Streaming.Pending.zero = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) (Complexity.SAT.ThreeSAT.Streaming.Pending.two a_1 b) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.one a) (Complexity.SAT.ThreeSAT.Streaming.Pending.three a_1 b c) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) Complexity.SAT.ThreeSAT.Streaming.Pending.zero = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) (Complexity.SAT.ThreeSAT.Streaming.Pending.one a_1) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b) (Complexity.SAT.ThreeSAT.Streaming.Pending.three a_1 b_1 c) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) Complexity.SAT.ThreeSAT.Streaming.Pending.zero = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) (Complexity.SAT.ThreeSAT.Streaming.Pending.one a_1) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqPending.decEq (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c) (Complexity.SAT.ThreeSAT.Streaming.Pending.two a_1 b_1) = isFalse ⋯

def Complexity.SAT.ThreeSAT.Streaming.Pending.toClause : Pending → Clause

Recover the clause represented by the bounded pending-literal state.

Equations

• Complexity.SAT.ThreeSAT.Streaming.Pending.zero.toClause = []
• (Complexity.SAT.ThreeSAT.Streaming.Pending.one a).toClause = [a]
• (Complexity.SAT.ThreeSAT.Streaming.Pending.two a b).toClause = [a, b]
• (Complexity.SAT.ThreeSAT.Streaming.Pending.three a b c).toClause = [a, b, c]

inductive Complexity.SAT.ThreeSAT.Streaming.Scan : Type

Token-parser state for a raw literal. The first data bit is its sign; every later data bit must be true and increments the unary variable counter.

• boundary : Scan
• literal (sign : Bool) (var : ℕ) : Scan

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Streaming.instDecidableEqScan : DecidableEq Scan

Equations

• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqScan = Complexity.SAT.ThreeSAT.Streaming.instDecidableEqScan.decEq

def Complexity.SAT.ThreeSAT.Streaming.instDecidableEqScan.decEq (x✝ x✝¹ : Scan) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqScan.decEq Complexity.SAT.ThreeSAT.Streaming.Scan.boundary Complexity.SAT.ThreeSAT.Streaming.Scan.boundary = isTrue ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqScan.decEq Complexity.SAT.ThreeSAT.Streaming.Scan.boundary (Complexity.SAT.ThreeSAT.Streaming.Scan.literal sign var) = isFalse ⋯
• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqScan.decEq (Complexity.SAT.ThreeSAT.Streaming.Scan.literal sign var) Complexity.SAT.ThreeSAT.Streaming.Scan.boundary = isFalse ⋯

structure Complexity.SAT.ThreeSAT.Streaming.State : Type

State of the streaming transducer. emitted is an append-only token accumulator, and next is the first unused auxiliary-variable index.

• next : ℕ

  First unused auxiliary-variable index.

• pending : Pending

  At most three source literals waiting to be emitted.

• scan : Scan

  Current raw-literal parser state.

• emitted : List EncToken

  Append-only output-token accumulator.

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Streaming.instDecidableEqState : DecidableEq State

Equations

• Complexity.SAT.ThreeSAT.Streaming.instDecidableEqState = Complexity.SAT.ThreeSAT.Streaming.instDecidableEqState.decEq

def Complexity.SAT.ThreeSAT.Streaming.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

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

def Complexity.SAT.ThreeSAT.Streaming.initial (next : ℕ) : State

State at the beginning of a formula, before any token has been read.

Equations

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

def Complexity.SAT.ThreeSAT.Streaming.clauseTokens (c : Clause) : List EncToken

The token encoding of one completed output clause.

Equations

• Complexity.SAT.ThreeSAT.Streaming.clauseTokens c = Complexity.SAT.CNF.tokens [c]

def Complexity.SAT.ThreeSAT.Streaming.pushLiteral (st : State) (lit : Lit) : State

Incorporate a decoded source literal. The first three literals are kept; each later literal emits the next link of the Tseitin chain.

Equations

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

def Complexity.SAT.ThreeSAT.Streaming.closeClause (st : State) : State

Finish the current source clause. The bounded pending clause is handled by the same short-clause cases as Clause.to3CNF; the empty case consumes one fresh variable for its contradiction gadget.

Equations

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

def Complexity.SAT.ThreeSAT.Streaming.step (st : State) : EncToken → Option State

One token transition. It rejects malformed raw literals and separators in the middle of a literal. On valid CNF.tokens streams these cases are absent.

Equations

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

def Complexity.SAT.ThreeSAT.Streaming.run : State → List EncToken → Option State

Run the streaming transition over a token list.

Equations

• Complexity.SAT.ThreeSAT.Streaming.run x✝ [] = some x✝
• Complexity.SAT.ThreeSAT.Streaming.run x✝ (tok :: toks) = do let st' ← Complexity.SAT.ThreeSAT.Streaming.step x✝ tok Complexity.SAT.ThreeSAT.Streaming.run st' toks

def Complexity.SAT.ThreeSAT.Streaming.finish : State → Option (List EncToken × ℕ)

Accept a completed formula only at a clause boundary with no pending literals. Valid CNF.tokens streams always have this shape.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Streaming.finish x✝ = none

def Complexity.SAT.ThreeSAT.Streaming.transformFrom? (next : ℕ) (toks : List EncToken) : Option (List EncToken × ℕ)

Transform a token stream using the supplied first fresh variable.

Equations

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

def Complexity.SAT.ThreeSAT.Streaming.transformTokens? (toks : List EncToken) : Option (List EncToken × ℕ)

Transform a token stream, choosing the first fresh variable as one more than the concrete source bit length.

Equations

• Complexity.SAT.ThreeSAT.Streaming.transformTokens? toks = Complexity.SAT.ThreeSAT.Streaming.transformFrom? (Complexity.SAT.encodeTokens toks).length.succ toks

def Complexity.SAT.ThreeSAT.Streaming.transformBits? (toks : List EncToken) : Option (List Bool × ℕ)

Bit-level output of transformTokens?, retaining the final fresh counter for the machine-level invariant.

Equations

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

theorem Complexity.SAT.ThreeSAT.Streaming.transformFrom?_tokens_internal (phi : CNF) (next : ℕ) : transformFrom? next phi.tokens = some ((CNF.to3Aux next phi).1.tokens, (CNF.to3Aux next phi).2)

On a valid encoded CNF token stream, the streaming transducer agrees exactly with CNF.to3Aux, including its final fresh-variable counter.

theorem Complexity.SAT.ThreeSAT.Streaming.transformTokens?_tokens_internal (phi : CNF) : transformTokens? phi.tokens = some ((CNF.to3Aux (phi.encode.length + 1) phi).1.tokens, (CNF.to3Aux (phi.encode.length + 1) phi).2)

transformTokens? uses source bit length plus one as its fresh start and emits exactly the corresponding typed Tseitin transformation.

theorem Complexity.SAT.ThreeSAT.Streaming.transformBits?_tokens_internal (phi : CNF) : transformBits? phi.tokens = some ((CNF.to3Aux (phi.encode.length + 1) phi).1.encode, (CNF.to3Aux (phi.encode.length + 1) phi).2)

Bit-level correctness of the streaming transducer on every valid CNF token stream.

theorem Complexity.SAT.ThreeSAT.Streaming.maxVar_lt_streamStart_internal (phi : CNF) : phi.maxVar < phi.encode.length + 1

The bit-length-derived start is strictly above every source variable.