The unit-propagation machine of a Horn formula

The program half of HORNSAT ≤ᶠᵒ[≤] DTMAccept, the deterministic machine bridge: the states, symbols and transitions of the deterministic machine computing the unit-propagation closure of a CNF instance and verifying it, on the tape laid out in DescriptiveComplexity.Problems.Machine.HornTape.

The program

  init:      at ⊢, dispatch – first check sweep if a clause exists, else accept
  chk(r, c):  sweep right, f := f ∧ (negIn c x → marked x)
  mark(r, c): sweep back left; if the check succeeded, mark the positive
              literal of c in passing
  … next clause; after the last clause, next round; after the last round …
  ver(c):     sweep, f := f ∨ (posIn c x ∧ marked x) ∨ (negIn c x ∧ ¬marked x),
              alternating direction; a failed clause leaves no transition
  accept     after the last verified clause – gated on the Horn condition

n rounds of one check-and-mark pass per clause compute the propagation closure DescriptiveComplexity.Forced (DescriptiveComplexity.forced_forcedIn_card is the stabilization), and the verification phase accepts exactly when the closure, read as an assignment, satisfies every clause – which for a Horn instance is satisfiability itself (DescriptiveComplexity.satisfiable_iff_forced_model).

The machine is deterministic everywhere – there is no guess phase – and DescriptiveComplexity.TMData.Deterministic for the constructed machine is part of the statement, not bookkeeping: it is what makes the image a potential yes-instance of DTMAccept at all. The instance is read exactly as by the SAT machine (DescriptiveComplexity.SatCl, DescriptiveComplexity.SatPos …, imported from DescriptiveComplexity.Problems.Machine.Hardness together with the clause-order machinery), and the only two additions are the element order (rounds walk it) and the Horn gate on the accept transition.

The elements of the machine

@[reducible, inline]

abbrev DescriptiveComplexity.HV (A : Type) : Type

The universe of the machine: tagged triples.

Equations

• DescriptiveComplexity.HV A = (DescriptiveComplexity.UPTag × (Fin 3 → A))

noncomputable def DescriptiveComplexity.cstH {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : UPTag) : HV A

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

Equations

• DescriptiveComplexity.cstH t = (t, fun (x : Fin 3) => DescriptiveComplexity.botA)

noncomputable def DescriptiveComplexity.oneH {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : UPTag) (a : A) : HV A

A tag carrying one element.

Equations

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

noncomputable def DescriptiveComplexity.twoH {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (t : UPTag) (a b : A) : HV A

A tag carrying two elements.

Equations

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

theorem DescriptiveComplexity.isMinTup3_bot {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : IsMinTup3 fun (x : Fin 3) => botA

Symbols

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The left-marker symbol.

Equations

• DescriptiveComplexity.symHStart = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.sStart

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The right-marker symbol.

Equations

• DescriptiveComplexity.symHEnd = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.sEnd

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symHBlank {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The blank symbol.

Equations

• DescriptiveComplexity.symHBlank = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.sBlank

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.symCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (m : Bool) (x : A) : HV A

The symbol of the cell of x, with mark m.

Equations

• DescriptiveComplexity.symCell m x = DescriptiveComplexity.oneH (if m = true then DescriptiveComplexity.UPTag.sM else DescriptiveComplexity.UPTag.sU) x

Positions

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The left-marker cell.

Equations

• DescriptiveComplexity.posHStart = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.pStart

@[reducible, inline]

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

The cell of the element x.

Equations

• DescriptiveComplexity.posHCell x = DescriptiveComplexity.oneH DescriptiveComplexity.UPTag.pCell x

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The right-marker cell.

Equations

• DescriptiveComplexity.posHEnd = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.pEnd

States

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHInit {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The dispatch state.

Equations

• DescriptiveComplexity.stHInit = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.qInit

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHChk {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (f : Bool) (r c : A) : HV A

Checking the clause c in round r, flag f.

Equations

• DescriptiveComplexity.stHChk f r c = DescriptiveComplexity.twoH (DescriptiveComplexity.UPTag.qChk f) r c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHMark {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (m : Bool) (r c : A) : HV A

The return sweep of clause c in round r, marking iff m.

Equations

• DescriptiveComplexity.stHMark m r c = DescriptiveComplexity.twoH (DescriptiveComplexity.UPTag.qMark m) r c

@[reducible, inline]

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

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

Equations

• DescriptiveComplexity.stHVer f d c = DescriptiveComplexity.oneH (DescriptiveComplexity.UPTag.qVer f d) c

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.stHAcc {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HV A

The accepting state.

Equations

• DescriptiveComplexity.stHAcc = DescriptiveComplexity.cstH DescriptiveComplexity.UPTag.qAcc

Reading the order of the elements

def DescriptiveComplexity.MinElt {A : Type} [LinearOrder A] (a : A) : Prop

a is the least element.

Equations

• DescriptiveComplexity.MinElt a = ∀ (b : A), a ≤ b

def DescriptiveComplexity.MaxElt {A : Type} [LinearOrder A] (a : A) : Prop

a is the greatest element.

Equations

• DescriptiveComplexity.MaxElt a = ∀ (b : A), b ≤ a

def DescriptiveComplexity.SuccElt {A : Type} [LinearOrder A] (a b : A) : Prop

b is the successor of a in the order of the elements: rounds walk this relation.

Equations

• DescriptiveComplexity.SuccElt a b = (a < b ∧ ∀ (z : A), a < z → b ≤ z)

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

The satisfaction test of the verification phase: the cell x, with mark m, satisfies the clause c under the marked assignment. This is DescriptiveComplexity.SatLit with the marks as the valuation.

Equations

• DescriptiveComplexity.MLit c x m = (DescriptiveComplexity.SatPos c x ∧ m = true ∨ DescriptiveComplexity.SatNeg c x ∧ m = false)

The transition table

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

Which tagged triples are transitions: the payload promises. Coordinates not pinned by the source state or the symbol read are pinned here, so that no junk element is a transition.

Equations

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

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

The state a transition applies in.

Equations

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

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

The symbol a transition reads.

Equations

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

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

The state a transition moves to. The check and verification sweeps branch on a first-order test of the source instance; each pair of branches is exclusive, which is what keeps the table functional.

Equations

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

def DescriptiveComplexity.HWrite {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (τ a : HV A) : Prop

The symbol a transition writes: only the return sweep of a successful check writes anything new, and only at the positive literal of its clause.

Equations

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

def DescriptiveComplexity.HRight {A : Type} (τ : HV A) : Prop

Which transitions move the head right.

Equations

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

def DescriptiveComplexity.HAcc {A : Type} (q : HV A) : Prop

Accepting states.

Equations

• DescriptiveComplexity.HAcc q = (q.1 = DescriptiveComplexity.UPTag.qAcc)

def DescriptiveComplexity.HStart {A : Type} [LinearOrder A] (q : HV A) : Prop

Start states: the dispatch state alone.

Equations

• DescriptiveComplexity.HStart q = (q.1 = DescriptiveComplexity.UPTag.qInit ∧ DescriptiveComplexity.IsMinTup3 q.2)

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

The unit-propagation machine of a CNF instance.

Equations

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

The machine is well formed

The machine is deterministic

There is no guess phase, so – unlike the SAT machine – the whole table is functional: the state and the symbol read pin the transition's tag up to promise-exclusive alternatives, the tag pins the payload, and the branching destinations and writes are separated by their first-order tests. This discharges the DescriptiveComplexity.TMData.Deterministic promise of the constructed instance, which is part of the correctness of the reduction.

theorem DescriptiveComplexity.oneH_eq_oneH_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : UPTag} {a a' : A} : oneH t a = oneH t' a' ↔ t = t' ∧ a = a'

theorem DescriptiveComplexity.twoH_eq_twoH_iff {A : Type} [LinearOrder A] [Finite A] [Nonempty A] {t t' : UPTag} {a a' b b' : A} : twoH t a b = twoH t' a' b' ↔ t = t' ∧ a = a' ∧ b = b'

The promise-exclusive alternatives

The positions of the tape, concretely

The dimension-3 mirror of the SAT machine's marker and cell lemmas: the left marker is the lowest position, cells follow in the order of their elements, the right marker closes the chain, and ranks are what the budget compares.

theorem DescriptiveComplexity.hPosn_posHStart {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HPosn posHStart

theorem DescriptiveComplexity.hPosn_posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : HPosn (posHCell x)

theorem DescriptiveComplexity.hPosn_posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : HPosn posHEnd

theorem DescriptiveComplexity.hTagTupleLe_refl {A : Type} [LinearOrder A] (p : HV A) : tagTupleLe p p

theorem DescriptiveComplexity.hTagTupleLe_of_tag_lt {A : Type} [LinearOrder A] {p q : HV A} (h : p.1 < q.1) : tagTupleLe p q

theorem DescriptiveComplexity.hTagTupleLe_tag_le {A : Type} [LinearOrder A] {p q : HV A} (h : tagTupleLe p q) : p.1 ≤ q.1

theorem DescriptiveComplexity.posHStart_le_posHCell {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe posHStart (posHCell x)

theorem DescriptiveComplexity.posHCell_le_posHEnd {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (x : A) : tagTupleLe (posHCell x) posHEnd

The intended run: marks and tapes

The machine's working state is a set of marked elements, as a Bool-valued assignment. Processing one clause – a check sweep and a return sweep – applies DescriptiveComplexity.procB to it: unconditionally, because when the check fails the inner conjunction is false and nothing is added, exactly as the machine's return sweep writes nothing when its marking bit is off.

noncomputable def DescriptiveComplexity.procB {A : Type} [FirstOrder.Language.sat.Structure A] (M : A → Bool) (c : A) : A → Bool

One clause processed on a marked set: if every negative literal of c is marked, its positive literals join the marks.

Equations

• DescriptiveComplexity.procB M c x = (M x || decide (DescriptiveComplexity.SatPos c x) && decide (∀ (y : A), DescriptiveComplexity.SatNeg c y → M y = true))

noncomputable def DescriptiveComplexity.hTape {A : Type} [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) : HV A → HV A

The tape carrying the marked set M: markers and blanks in place, the cell of y holding (y, M y). A junk cell tuple reads its initial, unmarked symbol forever – it is never written, so its value must not depend on M.

Equations

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

noncomputable def DescriptiveComplexity.markTape {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (M : A → Bool) (c : A) (p : HV A) : HV A → HV A

The tape during a return sweep of the clause c with the head at p, moving left: the cells strictly above the head have been processed, the rest still carry the old marks.

Equations

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

The intended run: configurations

noncomputable def DescriptiveComplexity.confHInit {A : Type} [LinearOrder A] [Finite A] [Nonempty A] : Config (HV A)

The initial configuration: the dispatch state at the left marker, all cells unmarked.

Equations

• DescriptiveComplexity.confHInit = { state := DescriptiveComplexity.stHInit, head := DescriptiveComplexity.posHStart, tape := DescriptiveComplexity.hTape fun (x : A) => false }

The flags and tapes along a sweep

The intended run: single steps

Ranks, sweeps, and one whole clause

The folds: what the rounds compute

inductive DescriptiveComplexity.ClauseFold {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] : A → (A → Bool) → (A → Bool) → Prop

Processing the clauses from c to the last one, relationally: the marked set each clause leaves behind.

• last {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c : A} {M : A → Bool} : SatMaxCl c → ClauseFold c M (procB M c)
• step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c c' : A} {M M' : A → Bool} : SatNextCl c c' → ClauseFold c' (procB M c) M' → ClauseFold c M M'

inductive DescriptiveComplexity.RoundFold {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c₀ : A) : A → (A → Bool) → (A → Bool) → Prop

Processing the rounds from r to the last one, each a pass over all the clauses from c₀.

• last {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c₀ r : A} {M M' : A → Bool} : MaxElt r → ClauseFold c₀ M M' → RoundFold c₀ r M M'
• step {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {c₀ r r' : A} {M M' M'' : A → Bool} : SuccElt r r' → ClauseFold c₀ M M' → RoundFold c₀ r' M' M'' → RoundFold c₀ r M M''

The machine walks the folds

The verification phase

The machine accepts every Horn-satisfiable instance

theorem DescriptiveComplexity.hornMachine_final {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (hhorn : AtMostOnePositive A) (hsat : Satisfiable A) : ∃ (cfin : Config (HV A)) (n : ℕ) (M' : A → Bool), n < Nat.card { p : HV A // (hornMachine A).Posn p } ∧ (hornMachine A).StepsIn n confHInit cfin ∧ HAcc cfin.state ∧ cfin.tape = hTape M' ∧ ∀ (x : A), M' x = true ↔ Forced x

The run of the machine on a yes-instance of HORN-SAT: within the budget it reaches an accepting configuration – dispatch, n rounds of propagation, and a verification pass that the closure, which satisfiability makes a model, lets run to acceptance – and the tape then holds the marks of the propagation closure.

The machine accepts only Horn-satisfiable instances

Determinism replaces the SAT machine's run-analysis induction: the run from the unique initial configuration is the intended trajectory, so it suffices that on a non-Horn-satisfiable instance the trajectory never carries an accepting state – either because no accept transition exists at all (the Horn gate), or because the trajectory gets stuck at the first failing verification sweep.