Documentation

DescriptiveComplexity.Problems.Machine.Tape

The tape of the SAT machine #

The layout half of SAT ≤ᶠᵒ[≤] NTMAccept: which tagged tuples are positions, in what order they sit, and why there are enough of them. The program that runs on this tape – states, symbols, transitions – is separate.

The layout #

The machine's tape is one cell per element of the instance, bracketed by two markers, followed by filler cells that exist only to supply time:

  ⊢   x₁ x₂ … xₙ   ⊣   fillers…

Satisfiable assigns a truth value to every element (elements that are not variables of any clause are harmless), so there is no need to single out the variables: one cell per element is both simpler and correct.

Tags are ordered so that this is exactly the order of the interpreted universe. That order comes for free: DescriptiveComplexity.lexLeF is the defining formula of le – tags first, then the tuple lexicographically – and DescriptiveComplexity.tagTupleOrder is already a LinearOrder, so the well-formedness obligation IsLinOrd of DescriptiveComplexity.TMData.WellFormed is discharged without a single tag-pair case.

Only the position tags are fixed here. The symbol, state and transition tags of the program get higher indices, which leaves the order of the positions undisturbed – DescriptiveComplexity.satTagIdx is what has to stay monotone, not the constructor list.

The budget #

The machine needs one sweep to guess an assignment and one sweep per clause to check it, so (m + 1) · (n + 2) steps for n elements and m ≤ n clauses. Eight filler tags at dimension two give 8n² positions on their own – no need to count the markers and cells – and DescriptiveComplexity.sat_budget says that is always more than the machine needs. Following the plan's advice on risk #3, the filler is over-provisioned rather than the bound tightened: nothing downstream depends on the constant, and an off-by-one here would only surface at the very end of the correctness proof.

The tags of the positions #

source
inductive DescriptiveComplexity.SatTag :
Type

The tags carrying the tape of the SAT machine. The order of the constructors is the order of the tape; DescriptiveComplexity.satTagIdx is what makes that official.

The program's tags (symbols, states, transitions) will be added after these with higher indices, which does not disturb the order of the positions.

  • pStart : SatTag

    The left marker cell.

  • pCell : SatTag

    The cell of an element: one per element of the instance.

  • pEnd : SatTag

    The right marker cell.

  • pFill (i : Fin 8) : SatTag

    Filler cells, eight tags' worth, supplying the time budget.

  • sStart : SatTag

    The left-marker symbol ⊢.

  • sEnd : SatTag

    The right-marker symbol ⊣.

  • sBlank : SatTag

    The blank symbol.

  • sU : SatTag

    The symbol (x, U): the cell of x, not yet assigned.

  • sT : SatTag

    The symbol (x, T): the cell of x, assigned true.

  • sF : SatTag

    The symbol (x, F): the cell of x, assigned false.

  • qGuess : SatTag

    The guessing state.

  • qChk (f d : Bool) : SatTag

    Checking clause c with the accumulated flag f, sweeping in direction d (true = rightwards).

  • qAcc : SatTag

    The accepting state.

  • tGuessStart : SatTag

    Guess phase: step over the left marker.

  • tGuessVal (b : Bool) : SatTag

    Guess phase: write the truth value b in an unassigned cell.

  • tGuessEndAcc : SatTag

    Guess phase over, and there is no clause: accept.

  • tGuessEndChk : SatTag

    Guess phase over: start checking the lowest clause.

  • tChk (b f d : Bool) : SatTag

    Check phase: read (x, b) with flag f, sweeping in direction d.

  • tTurnNext (d : Bool) : SatTag

    Check phase: the clause is satisfied and another one follows.

  • tTurnAcc (d : Bool) : SatTag

    Check phase: the clause is satisfied and it was the last one.

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.instDecidableEqSatTag :
    DecidableEq SatTag
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.instDecidableEqSatTag.decEq (x✝ x✝¹ : SatTag) :
    Decidable (x✝ = x✝¹)
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      instance DescriptiveComplexity.instFintypeSatTag :
      Fintype SatTag
      Equations
      • One or more equations did not get rendered due to their size.
      Dependency graph
      source
      instance DescriptiveComplexity.instNonemptySatTag :
      Nonempty SatTag
      Dependency graph
      source
      def DescriptiveComplexity.satTagIdx :
      SatTag → ℕ

      The position of a tag in the tape order.

      Equations
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.satTagIdx_injective :
        Function.Injective satTagIdx
        Dependency graph
        source
        @[instance_reducible]
        instance DescriptiveComplexity.instLinearOrderSatTag :
        LinearOrder SatTag

        The tape order on tags.

        Equations
        Dependency graph

        The intended positions #

        Stated as a plain predicate on tagged tuples, in the style of DescriptiveComplexity.IAdjRaw: the interpretation's posn formula will be shown to realize exactly this, and every fact proved here transfers.

        source
        def DescriptiveComplexity.SatPosn {A : Type} [LinearOrder A] (p : SatTag × (Fin 2 → A)) :
        Prop

        The tagged tuples that are positions: the two markers are the single tuple of minima, an element's cell is that element in the first coordinate, and the fillers are unrestricted.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph

          The instance data of the machine #

          The order, the blank symbol and the initial tape – everything DescriptiveComplexity.TMData.WellFormed asks about, which is therefore discharged here once, before any transition exists.

          source
          def DescriptiveComplexity.IsMinTup {A : Type} [LinearOrder A] (w : Fin 2 → A) :
          Prop

          The tuple of minima: the coordinates a marker or a constant symbol is pinned to, so that exactly one tuple carries such a tag.

          Equations
          Instances For
            Dependency graph
            source
            theorem DescriptiveComplexity.isMinTup_unique {A : Type} [LinearOrder A] {w w' : Fin 2 → A} (h : IsMinTup w) (h' : IsMinTup w') :
            w = w'
            Dependency graph
            source
            theorem DescriptiveComplexity.exists_isMinTup {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :
            ∃ (w : Fin 2 → A), IsMinTup w
            Dependency graph
            source
            def DescriptiveComplexity.SatBlank {A : Type} [LinearOrder A] (p : SatTag × (Fin 2 → A)) :
            Prop

            The blank symbol: one element, pinned to the tuple of minima.

            Equations
            Instances For
              Dependency graph
              source
              theorem DescriptiveComplexity.exists_satBlank {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :
              ∃ (p : SatTag × (Fin 2 → A)), SatBlank p
              Dependency graph
              source
              theorem DescriptiveComplexity.satBlank_unique {A : Type} [LinearOrder A] {p q : SatTag × (Fin 2 → A)} (hp : SatBlank p) (hq : SatBlank q) :
              p = q
              Dependency graph
              source
              def DescriptiveComplexity.SatInp {A : Type} [LinearOrder A] (p a : SatTag × (Fin 2 → A)) :
              Prop

              The initial tape: the markers hold their own symbols, the cell of an element holds that element still unassigned, and the fillers hold nothing – so the blank, by DescriptiveComplexity.TMData.InitTape.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Dependency graph
                source
                theorem DescriptiveComplexity.satInp_functional {A : Type} [LinearOrder A] {p a b : SatTag × (Fin 2 → A)} (ha : SatInp p a) (hb : SatInp p b) :
                a = b

                The initial tape is functional: a cell holds at most one symbol. The three cases are separated by the tag of the cell, and within each case the symbol's tuple is pinned.

                Dependency graph
                source
                theorem DescriptiveComplexity.exists_satPosn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :
                ∃ (p : SatTag × (Fin 2 → A)), SatPosn p

                There is a position: the start marker.

                Dependency graph
                source
                theorem DescriptiveComplexity.isLinOrd_tagTupleLe {A : Type} [LinearOrder A] :
                IsLinOrd tagTupleLe

                The interpreted order is linear, from DescriptiveComplexity.tagTupleOrder – no tag-pair case analysis.

                Dependency graph

                The budget #

                source
                theorem DescriptiveComplexity.sat_budget {n m : ℕ} (hn : 1 ≤ n) (hm : m ≤ n) :
                (m + 1) * (n + 2) < 8 * n * n

                The filler cells alone are enough. The machine takes one sweep to guess an assignment and one per clause to check it, (m + 1) · (n + 2) steps in all for n elements and m ≤ n clauses; the eight filler tags contribute 8n² positions by themselves, so no count of the markers and cells is needed.

                The inequality is strict, as DescriptiveComplexity.TMData.Accepts requires: N positions are N time points and so N - 1 steps.

                Dependency graph
                source
                theorem DescriptiveComplexity.card_le_card_posn (A : Type) [LinearOrder A] [Finite A] :
                8 * Nat.card A * Nat.card A ≤ Nat.card { p : SatTag × (Fin 2 → A) // SatPosn p }

                The tape really has that many positions: the filler tuples alone inject into the positions, which is all the budget argument needs.

                Dependency graph