The machine of a CNF formula

The program half of SAT ≤ᶠᵒ[≤] NTMAccept: the states, symbols and transitions of the machine M_φ built inside an ordered SAT instance, on the tape laid out in DescriptiveComplexity.Problems.Machine.Tape.

The program

  guess :  ⊢ →  at each cell (x,U) write (x,F), or (x,T) if x occurs in a
                clause, moving right  → ⊣
  check c: sweep back over the cells, accumulating
             flag := flag ∨ (posIn c x ∧ b) ∨ (negIn c x ∧ ¬b)
           at the far marker: if flag, take the next clause and turn round;
                              if not, no transition exists and the run dies
  accept:  when the clause just checked was the last one

Two things make this small. The check is an first-order test on the source structure – DescriptiveComplexity.SatLit – evaluated by the formula that will define the transition relation, so no clause-width bound and no occurrence machinery are needed and the source can be plain SAT rather than 3SAT. And the sweeps alternate direction instead of rewinding, so a clause costs one pass and there are no rewind states; the markers are what tell the machine a pass has ended.

The machine is nondeterministic in exactly one place, the choice of (x,T) or (x,F) in the guess phase, and it has that choice only at an element that is a variable of the instance (DescriptiveComplexity.SatVar): elsewhere it writes (x,F). The decision problem does not need this restriction; it is what makes the accepting runs correspond one to one to the models of the formula (DescriptiveComplexity.Problems.Machine.CountingHardness). Branching at the guess only is a deliberate design decision, and it is what will make the ⇒ half of correctness a corollary of uniqueness rather than a second invariant induction.

Semantics first

Everything here is a plain predicate on tagged tuples, as DescriptiveComplexity.SatPosn and DescriptiveComplexity.SatInp are: the machine is assembled as a DescriptiveComplexity.TMData and reasoned about directly. Only once its correctness is proved does the first-order transcription happen, one realization lemma per relFormula. A transition table type-checks whatever it says, so it has to be validated by a proof, not by elaboration.

The instance, read

def DescriptiveComplexity.SatCl {A : Type} [FirstOrder.Language.sat.Structure A] (c : A) : Prop

Being a clause of the CNF instance.

Equations

• DescriptiveComplexity.SatCl c = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satIsClause ![c]

def DescriptiveComplexity.SatPos {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) : Prop

The variable x occurs positively in the clause c.

Equations

• DescriptiveComplexity.SatPos c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satPosIn ![c, x]

def DescriptiveComplexity.SatNeg {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) : Prop

The variable x occurs negatively in the clause c.

Equations

• DescriptiveComplexity.SatNeg c x = FirstOrder.Language.Structure.RelMap FirstOrder.Language.satNegIn ![c, x]

def DescriptiveComplexity.SatLit {A : Type} [FirstOrder.Language.sat.Structure A] (c x : A) (v : Bool) : Prop

The literal test: the cell x, holding the truth value v, satisfies the clause c. This is the first-order test on the source structure that the transition relation performs; it is the whole of the check phase.

Equations

• DescriptiveComplexity.SatLit c x v = (DescriptiveComplexity.SatPos c x ∧ v = true ∨ DescriptiveComplexity.SatNeg c x ∧ v = false)

def DescriptiveComplexity.SatVar {A : Type} [FirstOrder.Language.sat.Structure A] (x : A) : Prop

The element x is a variable of the instance: it occurs in some clause. The machine guesses a truth value only at such an element, and writes “false” at the others, so that its accepting runs are the models of the formula and not its satisfying assignments of all elements.

Equations

• DescriptiveComplexity.SatVar x = ∃ (c : A), DescriptiveComplexity.SatCl c ∧ (DescriptiveComplexity.SatPos c x ∨ DescriptiveComplexity.SatNeg c x)

def DescriptiveComplexity.SatMinCl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : Prop

c is the lowest clause.

Equations

• DescriptiveComplexity.SatMinCl c = (DescriptiveComplexity.SatCl c ∧ ∀ (e : A), DescriptiveComplexity.SatCl e → c ≤ e)

def DescriptiveComplexity.SatMaxCl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : Prop

c is the highest clause.

Equations

• DescriptiveComplexity.SatMaxCl c = (DescriptiveComplexity.SatCl c ∧ ∀ (e : A), DescriptiveComplexity.SatCl e → e ≤ c)

def DescriptiveComplexity.SatNextCl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c c' : A) : Prop

c' is the clause immediately above c.

Equations

• DescriptiveComplexity.SatNextCl c c' = (DescriptiveComplexity.SatCl c ∧ DescriptiveComplexity.SatCl c' ∧ c < c' ∧ ∀ (e : A), DescriptiveComplexity.SatCl e → c < e → c' ≤ e)

The elements of the machine

noncomputable def DescriptiveComplexity.botA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : A

The least element of the instance, to which every constant of the machine is pinned.

Equations

• DescriptiveComplexity.botA = ⋯.choose

theorem DescriptiveComplexity.botA_le {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : botA ≤ a

theorem DescriptiveComplexity.isMinTup_bot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : IsMinTup fun (x : Fin 2) => botA

@[reducible, inline]

abbrev DescriptiveComplexity.SatV (A : Type) : Type

The universe of the machine: tagged pairs.

Equations

• DescriptiveComplexity.SatV A = (DescriptiveComplexity.SatTag × (Fin 2 → A))

noncomputable def DescriptiveComplexity.cst {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : SatTag) : SatV A

A constant of the machine: a tag on the pair of least elements.

Equations

• DescriptiveComplexity.cst t = (t, fun (x : Fin 2) => DescriptiveComplexity.botA)

noncomputable def DescriptiveComplexity.one {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : SatTag) (a : A) : SatV A

A tag carrying one element, pinned in the second coordinate.

Equations

• DescriptiveComplexity.one t a = (t, ![a, DescriptiveComplexity.botA])

Symbols

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The left-marker symbol.

Equations

• DescriptiveComplexity.symStart = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.sStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The right-marker symbol.

Equations

• DescriptiveComplexity.symEnd = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.sEnd

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symBlank {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The blank symbol.

Equations

• DescriptiveComplexity.symBlank = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.sBlank

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symU {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : SatV A

The symbol of an unassigned cell.

Equations

• DescriptiveComplexity.symU x = DescriptiveComplexity.one DescriptiveComplexity.SatTag.sU x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symV {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (v : Bool) (x : A) : SatV A

The symbol of a cell assigned the truth value v.

Equations

• DescriptiveComplexity.symV v x = DescriptiveComplexity.one (if v = true then DescriptiveComplexity.SatTag.sT else DescriptiveComplexity.SatTag.sF) x

Positions

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The left-marker cell.

Equations

• DescriptiveComplexity.posStart = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.pStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : SatV A

The cell of the element x.

Equations

• DescriptiveComplexity.posCell x = DescriptiveComplexity.one DescriptiveComplexity.SatTag.pCell x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The right-marker cell.

Equations

• DescriptiveComplexity.posEnd = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.pEnd

States

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stGuess {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The guessing state.

Equations

• DescriptiveComplexity.stGuess = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.qGuess

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stChk {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f d : Bool) (c : A) : SatV A

Checking the clause c, flag f, sweeping in direction d.

Equations

• DescriptiveComplexity.stChk f d c = DescriptiveComplexity.one (DescriptiveComplexity.SatTag.qChk f d) c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stAcc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : SatV A

The accepting state.

Equations

• DescriptiveComplexity.stAcc = DescriptiveComplexity.cst DescriptiveComplexity.SatTag.qAcc

The transition table

def DescriptiveComplexity.SatTr {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (τ : SatV A) : Prop

Which tagged tuples are transitions. The payload is pinned exactly as far as the transition needs it, and the clause coordinates are required to be clauses, so that no junk element is ever a transition.

Equations

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

def DescriptiveComplexity.SatSrc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ q : SatV A) : Prop

The state a transition applies in.

Equations

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

def DescriptiveComplexity.SatRead {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : SatV A) : Prop

The symbol a transition reads.

Equations

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

def DescriptiveComplexity.SatDst {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ q : SatV A) : Prop

The state a transition moves to. The only place the instance is consulted is the check clause, where the new flag depends on DescriptiveComplexity.SatLit.

Equations

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

def DescriptiveComplexity.SatWrite {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (τ a : SatV A) : Prop

The symbol a transition writes: everything but the guess phase leaves the tape as it found it.

Equations

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

def DescriptiveComplexity.SatRight {A : Type} (τ : SatV A) : Prop

Which transitions move the head right: the guess phase always does, a check sweep goes in its own direction, and a turn – whether it takes the next clause or accepts – reverses. A turn must reverse even when accepting: it fires at a marker, and there is no position beyond one.

Equations

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

def DescriptiveComplexity.SatAcc {A : Type} (q : SatV A) : Prop

Accepting states: just DescriptiveComplexity.stAcc.

Equations

• DescriptiveComplexity.SatAcc q = (q.1 = DescriptiveComplexity.SatTag.qAcc)

def DescriptiveComplexity.SatStart {A : Type} [LinearOrder A] (q : SatV A) : Prop

Start states: just DescriptiveComplexity.stGuess.

Equations

• DescriptiveComplexity.SatStart q = (q.1 = DescriptiveComplexity.SatTag.qGuess ∧ DescriptiveComplexity.IsMinTup q.2)

def DescriptiveComplexity.satMachine (A : Type) [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : TMData (SatV A)

The machine of a CNF instance.

Equations

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

The table is a table

Before any run is considered: each transition has exactly one destination and symbol written, and the two places where two tags could otherwise both apply are exclusive. A mistake in the table shows up here first, which is why these come before the correctness proof. (Sources and symbols read need no functionality lemma of their own: DescriptiveComplexity.satTr_unique pins the whole transition from them.)

theorem DescriptiveComplexity.one_eq_one_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : SatTag} {a a' : A} : one t a = one t' a' ↔ t = t' ∧ a = a'

theorem DescriptiveComplexity.satTr_unique {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {τ τ' q a : SatV A} (hτ : SatTr τ) (hτ' : SatTr τ') (hs : SatSrc τ q) (hs' : SatSrc τ' q) (hr : SatRead τ a) (hr' : SatRead τ' a) (hguess : ¬(q = stGuess ∧ ∃ (x : A), a = symU x)) : τ = τ'

At most one transition applies, away from the one nondeterministic choice of the guess phase: the state and the symbol read pin the tag (DescriptiveComplexity.tag_cases), the tag pins the payload (DescriptiveComplexity.satTr_payload), and the three ambiguities are the guess itself and the two exclusive branch points.

The positions of the tape, concretely

noncomputable def DescriptiveComplexity.topA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : A

The greatest element of the instance: the last cell of the tape.

Equations

• DescriptiveComplexity.topA = ⋯.choose

theorem DescriptiveComplexity.le_topA {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (a : A) : a ≤ topA

theorem DescriptiveComplexity.step_functional_off_guess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {c c₁ c₂ : Config (SatV A)} (hguess : ¬(c.state = stGuess ∧ ∃ (x : A), c.tape c.head = symU x)) (h₁ : (satMachine A).Step c c₁) (h₂ : (satMachine A).Step c c₂) : c₁ = c₂

The machine is deterministic away from the guess. Once the transition is pinned (DescriptiveComplexity.satTr_unique), the successor configuration is too: its state by satDst_functional, the cell under the head by satWrite_functional, every other cell by the frame condition, and the head itself by uniqueness of the neighbor in the direction the transition names.

This is a deliberate design decision: with only the guess phase branching, the ⇒ half of correctness becomes a corollary of uniqueness rather than a second invariant induction.

What a step leaves alone

Three facts about arbitrary steps, which the counting form of the correctness proof needs (DescriptiveComplexity.Problems.Machine.CountingHardness): only a guess write changes the tape, the guessing state is never entered again once left, and an accepting configuration has no successor.

The intended run: the guess phase

noncomputable def DescriptiveComplexity.guessTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (p q : SatV A) : SatV A

The tape during the guess sweep, with the head at p: the markers hold their own symbols, a cell strictly below the head has been assigned its value under ν, a cell at or above the head is still unassigned, and every other element reads blank.

A tuple carrying a cell's tag but a junk second coordinate is not a position, and the machine never visits it – but the frame condition of a step quantifies over it all the same, so its value must not move as the head advances. Hence the guard ∀ a, q.2 1 ≤ a: junk cells read unassigned forever, which is also what DescriptiveComplexity.SatInp says they hold initially.

Equations

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

noncomputable def DescriptiveComplexity.confGuess {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) (p : SatV A) : Config (SatV A)

The configuration during the guess sweep, with the head at p.

Equations

• DescriptiveComplexity.confGuess ν p = { state := DescriptiveComplexity.stGuess, head := p, tape := DescriptiveComplexity.guessTape ν p }

The intended run: a check sweep

noncomputable def DescriptiveComplexity.doneTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (ν : A → Bool) : SatV A → SatV A

The tape once the guess sweep has finished: every cell assigned. It does not change again, so the frame condition of every later step is rfl.

Equations

• DescriptiveComplexity.doneTape ν = DescriptiveComplexity.guessTape ν DescriptiveComplexity.posEnd

One clause, checked end to end

Each of these is a sweep followed by its turn. They are the step and the base case of the induction over clauses; the induction itself only has to choose between them. Each carries its step count, bounded by the rank of the right marker: that is the honest per-clause cost, roughly the size of the instance, and what lets the whole run fit the budget of DescriptiveComplexity.TMData.Accepts.

Correctness, the chaining half

Correctness, from an accepting run to an assignment

By design, the machine branches only at the guess, so an accepting run is the intended run of the assignment it wrote, and the flag conditions along it force every clause to be satisfied. The analysis is one induction on the length of the run, with one case per tag of the head position. At each non-guess configuration the transition that fired is identified through its tag – a decide over the finite tag type – and the actual step is equated with the intended one by DescriptiveComplexity.step_functional_off_guess; at a guess configuration the transition itself says which value was written.

theorem DescriptiveComplexity.sat_of_guess {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (k : ℕ) (ν : A → Bool) (p : SatV A) (cfin : Config (SatV A)) : (∀ (x : A), ν x = true → SatVar x) → SatPosn p → tagTupleLe p posEnd → (satMachine A).StepsIn k (confGuess ν p) cfin → SatAcc cfin.state → ∃ (ν' : A → Bool), (∀ (x : A), ν' x = true → SatVar x) ∧ (∀ (e : A), SatCl e → ∃ (y : A), SatLit e y (ν' y)) ∧ cfin.tape = doneTape ν'

The guess-phase analysis: an accepting run from a guess configuration yields a satisfying assignment. Walking the guess sweep, the assignment is rebuilt one cell at a time from the values the run chose to write; at the right marker the run either accepts – no clause exists – or enters the check phase, where DescriptiveComplexity.sat_of_chk takes over.

The machine accepts exactly the satisfiable instances

theorem DescriptiveComplexity.satMachine_accepts_iff_satisfiable {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : (satMachine A).Accepts ↔ Satisfiable A

Correctness of the machine of a CNF formula: it accepts – within the budget – exactly the satisfiable instances.