Machine building blocks for the CNF-to-3CNF reduction

This file starts the concrete deterministic-machine implementation of ThreeSAT.reduction. The first pass is a finite-state syntax validator for the concrete two-bit SAT encoding. No output from the transformation is emitted before that pass succeeds. The machine then rewinds the input and can enter a valid-input streaming emitter; malformed inputs take a fixed branch that emits ThreeSAT.fallbackEncoding.

The six work tapes have fixed roles. The fresh-variable register is initialized to |z| + 1, and four further registers hold the current literal and the three pending literals used by the streaming Tseitin algorithm. This file also gives the concrete register-copy and emission machines for committing a literal, emitting a wide-clause link, and closing a clause. Machine.Controller supplies the finite-state controller that reads validated tokens and schedules these machines.

Main definitions

• ValidationState — bit-pair syntax-validator state
• validationTM — concrete one-pass validation machine
• PendingSigns — finite-control signs for the three literal buffers
• commitLiteralTM — buffer or emit one decoded literal
• closeClauseTM — emit the completed exact-3 clause gadget
• seedFreshTM — initialize the fresh register to |z| + 1
• reductionTMWith — validate first, then branch to an emitter or fallback

Finite-state validation

inductive Complexity.SAT.ThreeSAT.Machine.ValidationMode : Type

Token-parser information retained by the regular syntax validator.

between hasLiteral means that no literal is currently open; hasLiteral records whether the current clause already contains a completed literal. literal hasLiteral means that a sign bit has been read and every subsequent raw bit seen so far was true.

• between (hasLiteral : Bool) : ValidationMode
• literal (hasLiteral : Bool) : ValidationMode
• reject : ValidationMode

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationMode : DecidableEq ValidationMode

Equations

• Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationMode = Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationMode.decEq

def Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationMode.decEq (x✝ x✝¹ : ValidationMode) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationMode.decEq Complexity.SAT.ThreeSAT.Machine.ValidationMode.reject Complexity.SAT.ThreeSAT.Machine.ValidationMode.reject = isTrue ⋯

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instFintypeValidationMode : Fintype ValidationMode

Equations

• Complexity.SAT.ThreeSAT.Machine.instFintypeValidationMode = Fintype.ofEquiv (Bool ⊕ Bool ⊕ Unit) Complexity.SAT.ThreeSAT.Machine.ValidationMode.proxyTypeEquiv

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instReprValidationMode : Repr ValidationMode

Equations

• Complexity.SAT.ThreeSAT.Machine.instReprValidationMode = { reprPrec := Complexity.SAT.ThreeSAT.Machine.instReprValidationMode.repr }

def Complexity.SAT.ThreeSAT.Machine.instReprValidationMode.repr : ValidationMode → ℕ → Std.Format

Equations

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

def Complexity.SAT.ThreeSAT.Machine.tokenOfPair : Bool → Bool → EncToken

Decode one concrete pair of input bits as a SAT encoding token.

Equations

• Complexity.SAT.ThreeSAT.Machine.tokenOfPair false false = Complexity.SAT.EncToken.bit false
• Complexity.SAT.ThreeSAT.Machine.tokenOfPair true true = Complexity.SAT.EncToken.bit true
• Complexity.SAT.ThreeSAT.Machine.tokenOfPair false true = Complexity.SAT.EncToken.litSep
• Complexity.SAT.ThreeSAT.Machine.tokenOfPair true false = Complexity.SAT.EncToken.clauseSep

def Complexity.SAT.ThreeSAT.Machine.ValidationMode.step : ValidationMode → EncToken → ValidationMode

One token transition of the syntax validator.

Equations

• (Complexity.SAT.ThreeSAT.Machine.ValidationMode.between seen).step (Complexity.SAT.EncToken.bit b) = Complexity.SAT.ThreeSAT.Machine.ValidationMode.literal seen
• (Complexity.SAT.ThreeSAT.Machine.ValidationMode.between hasLiteral).step Complexity.SAT.EncToken.litSep = Complexity.SAT.ThreeSAT.Machine.ValidationMode.reject
• (Complexity.SAT.ThreeSAT.Machine.ValidationMode.between hasLiteral).step Complexity.SAT.EncToken.clauseSep = Complexity.SAT.ThreeSAT.Machine.ValidationMode.between false
• (Complexity.SAT.ThreeSAT.Machine.ValidationMode.literal seen).step (Complexity.SAT.EncToken.bit true) = Complexity.SAT.ThreeSAT.Machine.ValidationMode.literal seen
• (Complexity.SAT.ThreeSAT.Machine.ValidationMode.literal hasLiteral).step (Complexity.SAT.EncToken.bit false) = Complexity.SAT.ThreeSAT.Machine.ValidationMode.reject
• (Complexity.SAT.ThreeSAT.Machine.ValidationMode.literal hasLiteral).step Complexity.SAT.EncToken.litSep = Complexity.SAT.ThreeSAT.Machine.ValidationMode.between true
• (Complexity.SAT.ThreeSAT.Machine.ValidationMode.literal hasLiteral).step Complexity.SAT.EncToken.clauseSep = Complexity.SAT.ThreeSAT.Machine.ValidationMode.reject
• Complexity.SAT.ThreeSAT.Machine.ValidationMode.reject.step x✝ = Complexity.SAT.ThreeSAT.Machine.ValidationMode.reject

inductive Complexity.SAT.ThreeSAT.Machine.ValidationState : Type

Bit-level state: either waiting for the first or the second bit of a two-bit token. Ending in second rejects odd-length inputs.

• first (mode : ValidationMode) : ValidationState
• second (mode : ValidationMode) (firstBit : Bool) : ValidationState

def Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationState.decEq (x✝ x✝¹ : ValidationState) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationState : DecidableEq ValidationState

Equations

• Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationState = Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationState.decEq

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instFintypeValidationState : Fintype ValidationState

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instReprValidationState : Repr ValidationState

Equations

• Complexity.SAT.ThreeSAT.Machine.instReprValidationState = { reprPrec := Complexity.SAT.ThreeSAT.Machine.instReprValidationState.repr }

def Complexity.SAT.ThreeSAT.Machine.instReprValidationState.repr : ValidationState → ℕ → Std.Format

Equations

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

def Complexity.SAT.ThreeSAT.Machine.ValidationState.initial : ValidationState

Initial state of the validation scan.

Equations

• Complexity.SAT.ThreeSAT.Machine.ValidationState.initial = Complexity.SAT.ThreeSAT.Machine.ValidationState.first (Complexity.SAT.ThreeSAT.Machine.ValidationMode.between false)

def Complexity.SAT.ThreeSAT.Machine.ValidationState.step : ValidationState → Bool → ValidationState

Consume one concrete input bit.

Equations

• One or more equations did not get rendered due to their size.
• (Complexity.SAT.ThreeSAT.Machine.ValidationState.first mode).step x✝ = Complexity.SAT.ThreeSAT.Machine.ValidationState.second mode x✝

def Complexity.SAT.ThreeSAT.Machine.ValidationState.accepts : ValidationState → Bool

A scan accepts only between clauses, with no unfinished current clause.

Equations

• (Complexity.SAT.ThreeSAT.Machine.ValidationState.first (Complexity.SAT.ThreeSAT.Machine.ValidationMode.between false)).accepts = true
• x✝.accepts = false

def Complexity.SAT.ThreeSAT.Machine.validEncoding (z : List Bool) : Bool

Executable finite-state validity check for concrete SAT encodings.

Equations

• Complexity.SAT.ThreeSAT.Machine.validEncoding z = (List.foldl Complexity.SAT.ThreeSAT.Machine.ValidationState.step Complexity.SAT.ThreeSAT.Machine.ValidationState.initial z).accepts

inductive Complexity.SAT.ThreeSAT.Machine.ValidationPhase : Type

Control state of validationTM.

• scan (state : ValidationState) : ValidationPhase
• done : ValidationPhase

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationPhase : DecidableEq ValidationPhase

Equations

• Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationPhase = Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationPhase.decEq

def Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationPhase.decEq (x✝ x✝¹ : ValidationPhase) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.instDecidableEqValidationPhase.decEq Complexity.SAT.ThreeSAT.Machine.ValidationPhase.done Complexity.SAT.ThreeSAT.Machine.ValidationPhase.done = isTrue ⋯

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instFintypeValidationPhase : Fintype ValidationPhase

Equations

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

def Complexity.SAT.ThreeSAT.Machine.validationTM {n : ℕ} : TM n

Scan the input from its current left boundary, returning 1 exactly when the bit-pair syntax is a complete CNF encoding. The start-marker case lets the same machine run both from an initial configuration and after seedFreshTM, where the input is already parked at cell one. Work tapes are preserved.

Equations

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

Fixed work-tape layout

@[reducible, inline]

abbrev Complexity.SAT.ThreeSAT.Machine.workTapeCount : ℕ

Number of work tapes used by the streaming reduction.

Equations

• Complexity.SAT.ThreeSAT.Machine.workTapeCount = 6

def Complexity.SAT.ThreeSAT.Machine.freshReg : Fin workTapeCount

Unary register containing the first unused auxiliary variable.

Equations

• Complexity.SAT.ThreeSAT.Machine.freshReg = ⟨0, Complexity.SAT.ThreeSAT.Machine.freshReg._proof_1⟩

def Complexity.SAT.ThreeSAT.Machine.currentReg : Fin workTapeCount

Unary register for the literal currently being scanned.

Equations

• Complexity.SAT.ThreeSAT.Machine.currentReg = ⟨1, Complexity.SAT.ThreeSAT.Machine.currentReg._proof_1⟩

def Complexity.SAT.ThreeSAT.Machine.bufferAReg : Fin workTapeCount

First pending-literal variable buffer.

Equations

• Complexity.SAT.ThreeSAT.Machine.bufferAReg = ⟨2, Complexity.SAT.ThreeSAT.Machine.bufferAReg._proof_1⟩

def Complexity.SAT.ThreeSAT.Machine.bufferBReg : Fin workTapeCount

Second pending-literal variable buffer.

Equations

• Complexity.SAT.ThreeSAT.Machine.bufferBReg = ⟨3, Complexity.SAT.ThreeSAT.Machine.bufferBReg._proof_1⟩

def Complexity.SAT.ThreeSAT.Machine.bufferCReg : Fin workTapeCount

Third pending-literal variable buffer.

Equations

• Complexity.SAT.ThreeSAT.Machine.bufferCReg = ⟨4, Complexity.SAT.ThreeSAT.Machine.bufferCReg._proof_1⟩

def Complexity.SAT.ThreeSAT.Machine.scratchReg : Fin workTapeCount

Scratch register reserved for controller-level copies and counters.

Equations

• Complexity.SAT.ThreeSAT.Machine.scratchReg = ⟨5, Complexity.SAT.ThreeSAT.Machine.scratchReg._proof_1⟩

inductive Complexity.SAT.ThreeSAT.Machine.PendingSigns : Type

Signs of the at most three source literals buffered in finite control. Their variable indices live in bufferAReg, bufferBReg, and bufferCReg.

• zero : PendingSigns
• one (a : Bool) : PendingSigns
• two (a b : Bool) : PendingSigns
• three (a b c : Bool) : PendingSigns

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instDecidableEqPendingSigns : DecidableEq PendingSigns

Equations

• Complexity.SAT.ThreeSAT.Machine.instDecidableEqPendingSigns = Complexity.SAT.ThreeSAT.Machine.instDecidableEqPendingSigns.decEq

def Complexity.SAT.ThreeSAT.Machine.instDecidableEqPendingSigns.decEq (x✝ x✝¹ : PendingSigns) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instFintypePendingSigns : Fintype PendingSigns

Equations

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

@[implicit_reducible]

instance Complexity.SAT.ThreeSAT.Machine.instReprPendingSigns : Repr PendingSigns

Equations

• Complexity.SAT.ThreeSAT.Machine.instReprPendingSigns = { reprPrec := Complexity.SAT.ThreeSAT.Machine.instReprPendingSigns.repr }

def Complexity.SAT.ThreeSAT.Machine.instReprPendingSigns.repr : PendingSigns → ℕ → Std.Format

Equations

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

Buffer and emission phases

def Complexity.SAT.ThreeSAT.Machine.emitClauseTM (aSign : Bool) (aReg : Fin workTapeCount) (bSign : Bool) (bReg : Fin workTapeCount) (cSign : Bool) (cReg : Fin workTapeCount) : TM workTapeCount

Emit one encoded clause with exactly three buffered literals.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.emitWideLinkTM (aSign bSign : Bool) : TM workTapeCount

Emit the first link of a wide clause: (a ∨ b ∨ fresh).

Equations

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

def Complexity.SAT.ThreeSAT.Machine.emitPendingTM : PendingSigns → TM workTapeCount

Emit the exact-3 gadget for the pending clause. The empty-clause case emits the contradictory positive/negative pair but does not yet increment the fresh register.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.clearBuffersTM : TM workTapeCount

Clear the current-literal register and all three pending buffers.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.rollWideBuffersTM : TM workTapeCount

Rotate the register buffers after emitting a wide-clause link.

Before the phase, the registers represent pending literals a,b,c, the current register contains d, and freshReg contains z. Afterwards the pending registers represent ¬z,c,d, the fresh register contains z+1, and the current register is zero.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.PendingSigns.push (pending : PendingSigns) (sign : Bool) : PendingSigns

Finite-control update paired with commitLiteralTM.

Equations

• Complexity.SAT.ThreeSAT.Machine.PendingSigns.zero.push sign = Complexity.SAT.ThreeSAT.Machine.PendingSigns.one sign
• (Complexity.SAT.ThreeSAT.Machine.PendingSigns.one a).push sign = Complexity.SAT.ThreeSAT.Machine.PendingSigns.two a sign
• (Complexity.SAT.ThreeSAT.Machine.PendingSigns.two a a_1).push sign = Complexity.SAT.ThreeSAT.Machine.PendingSigns.three a a_1 sign
• (Complexity.SAT.ThreeSAT.Machine.PendingSigns.three a a_1 a_2).push sign = Complexity.SAT.ThreeSAT.Machine.PendingSigns.three false a_2 sign

def Complexity.SAT.ThreeSAT.Machine.commitLiteralTM (pending : PendingSigns) : TM workTapeCount

Commit the decoded literal in currentReg.

The first three literals are copied into the pending buffers. Every later literal first emits (a ∨ b ∨ fresh), then rotates the buffers to (¬fresh,c,current) and increments freshReg.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.closeClauseTM (pending : PendingSigns) : TM workTapeCount

Emit and clear the current clause. Empty clauses consume one fresh variable; nonempty pending clauses consume no additional fresh variable.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SAT.ThreeSAT.Machine.closeClauseTM pending = (Complexity.SAT.ThreeSAT.Machine.emitPendingTM pending).seqTM (Complexity.TM.skipTM.seqTM Complexity.SAT.ThreeSAT.Machine.clearBuffersTM)

Validation-first assembly

def Complexity.SAT.ThreeSAT.Machine.seedFreshTM : TM workTapeCount

Initialize all tape heads, compute the source bit length in freshReg, and increment it. The resulting fresh counter is exactly |z| + 1.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.reductionFrontEndTM : TM workTapeCount

Run the fresh-counter initialization followed by the syntax validator. This is an executable front end for the reduction machine.

Equations

• Complexity.SAT.ThreeSAT.Machine.reductionFrontEndTM = Complexity.SAT.ThreeSAT.Machine.seedFreshTM.seqTM Complexity.SAT.ThreeSAT.Machine.validationTM

def Complexity.SAT.ThreeSAT.Machine.clearValidationOutputTM : TM workTapeCount

Blank the validator verdict at output cell one while preserving the input and every work register. The output head remains parked at cell one, ready for the append-only streaming emitter.

Equations

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

def Complexity.SAT.ThreeSAT.Machine.reductionTMWith (validEmitter : TM workTapeCount) : TM workTapeCount

Assemble the validation-first total reduction around a valid-input streaming emitter. The validator runs before either branch emits transformed data, and both branches clear its verdict before producing output. A valid input is rewound to cell one and handed to validEmitter; an invalid input emits the fixed no-instance fallbackEncoding. Machine.Controller supplies the concrete valid emitter used by the final reduction machine.

Equations

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