Documentation

DescriptiveComplexity.Problems.Machine.HornTape

The tape of the unit-propagation machine #

The layout half of HORNSAT ≤ᶠᵒ[≤] DTMAccept, stage 4 of the machine bridge: which tagged tuples are positions, in what order, and why there are enough of them. The program that runs on this tape is in DescriptiveComplexity.Problems.Machine.HornHardness.

The layout #

As for the SAT machine of stage 3: one cell per element of the instance, bracketed by two markers, followed by filler cells supplying time. The difference is the dimension: this machine does n propagation rounds of one check-and-mark pass per clause, O(n³) steps in all, so the interpreted universe is UPTag × A³ and sixteen filler tags give 16n³ positions.

A cell holds its element together with a mark – sU x unmarked, sM x marked – and the marked set is the machine's working copy of the unit propagation closure DescriptiveComplexity.Forced.

The program's tags #

All the machine's tags are declared here, as for stage 3: symbols, states and transitions get indices above the position tags, which leaves the order of the positions undisturbed. The states carry up to two elements – the current round and the current clause – which is what the third dimension of the payload accommodates.

The tags #

source
inductive DescriptiveComplexity.UPTag :
Type

The tags of the unit-propagation machine. Position tags first – their constructor order is the tape order – then symbols, states and transitions.

  • pStart : UPTag

    The left marker cell.

  • pCell : UPTag

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

  • pEnd : UPTag

    The right marker cell.

  • pFill (i : Fin 16) : UPTag

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

  • sStart : UPTag

    The left-marker symbol ⊢.

  • sEnd : UPTag

    The right-marker symbol ⊣.

  • sBlank : UPTag

    The blank symbol.

  • sU : UPTag

    The symbol (x, unmarked).

  • sM : UPTag

    The symbol (x, marked).

  • qInit : UPTag

    The dispatch state, at the left marker.

  • qChk (f : Bool) : UPTag

    Checking the current clause, sweeping right: f says every negative literal seen so far is marked. Payload: the round and the clause.

  • qMark (m : Bool) : UPTag

    The return sweep of a clause: m says the check succeeded, so the positive literal is marked in passing. Payload: the round and the clause.

  • qVer (f d : Bool) : UPTag

    Verifying the clause of the payload against the final marks, flag f, sweeping in direction d.

  • qAcc : UPTag

    The accepting state.

  • tInitChk : UPTag

    Dispatch: a clause exists, start the first check sweep.

  • tInitAcc : UPTag

    Dispatch: no clause at all, accept.

  • tChk (m f : Bool) : UPTag

    Check sweep: read a cell with mark m under flag f.

  • tChkEnd (f : Bool) : UPTag

    Check sweep over: turn round at ⊣ into the return sweep.

  • tMark (m mk : Bool) : UPTag

    Return sweep: read a cell with mark m; if mk, mark the positive literal of the clause in passing.

  • tMarkEndNext (mk : Bool) : UPTag

    Return sweep over, another clause follows in this round.

  • tMarkEndRound (mk : Bool) : UPTag

    Return sweep over, last clause, another round follows.

  • tMarkEndVer (mk : Bool) : UPTag

    Return sweep over, last clause of the last round: verification begins.

  • tVer (m f d : Bool) : UPTag

    Verification sweep: read a cell with mark m under flag f, sweeping in direction d.

  • tVerNext (d : Bool) : UPTag

    Verified: the clause is satisfied and another one follows.

  • tVerAcc (d : Bool) : UPTag

    Verified: the last clause is satisfied, and the instance is Horn.

Instances For
    Dependency graph
    source
    @[instance_reducible]
    instance DescriptiveComplexity.instDecidableEqUPTag :
    DecidableEq UPTag
    Equations
    Dependency graph
    source
    def DescriptiveComplexity.instDecidableEqUPTag.decEq (x✝ x✝¹ : UPTag) :
    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.instFintypeUPTag :
      Fintype UPTag
      Equations
      • One or more equations did not get rendered due to their size.
      Dependency graph
      source
      instance DescriptiveComplexity.instNonemptyUPTag :
      Nonempty UPTag
      Dependency graph
      source
      def DescriptiveComplexity.hTagIdx :
      UPTag → ℕ

      The position of a tag in the tape order.

      Equations
      Instances For
        Dependency graph
        source
        theorem DescriptiveComplexity.hTagIdx_injective :
        Function.Injective hTagIdx
        Dependency graph
        source
        @[instance_reducible]
        instance DescriptiveComplexity.instLinearOrderUPTag :
        LinearOrder UPTag

        The tape order on tags.

        Equations
        Dependency graph

        The intended positions #

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

        The tuple of minima at dimension three: what markers and constants are pinned to.

        Equations
        Instances For
          Dependency graph
          source
          theorem DescriptiveComplexity.isMinTup3_unique {A : Type} [LinearOrder A] {w w' : Fin 3 → A} (h : IsMinTup3 w) (h' : IsMinTup3 w') :
          w = w'
          Dependency graph
          source
          def DescriptiveComplexity.HPosn {A : Type} [LinearOrder A] (p : UPTag × (Fin 3 → A)) :
          Prop

          The tagged tuples that are positions: the markers on the triple of minima, an element's cell that element with a minimal rest, the fillers unrestricted.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Dependency graph
            source
            theorem DescriptiveComplexity.exists_isMinTup3 {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :
            ∃ (w : Fin 3 → A), IsMinTup3 w
            Dependency graph
            source
            def DescriptiveComplexity.HBlank {A : Type} [LinearOrder A] (p : UPTag × (Fin 3 → A)) :
            Prop

            The blank symbol of the machine: pinned to the triple of minima.

            Equations
            Instances For
              Dependency graph
              source
              theorem DescriptiveComplexity.exists_hBlank {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :
              ∃ (p : UPTag × (Fin 3 → A)), HBlank p
              Dependency graph
              source
              theorem DescriptiveComplexity.hBlank_unique {A : Type} [LinearOrder A] {p q : UPTag × (Fin 3 → A)} (hp : HBlank p) (hq : HBlank q) :
              p = q
              Dependency graph
              source
              def DescriptiveComplexity.HInp {A : Type} [LinearOrder A] (p a : UPTag × (Fin 3 → A)) :
              Prop

              The initial tape: the markers hold their own symbols and the cell of an element holds that element, unmarked.

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

                The initial tape is functional.

                Dependency graph
                source
                theorem DescriptiveComplexity.exists_hPosn {A : Type} [LinearOrder A] [Finite A] [Nonempty A] :
                ∃ (p : UPTag × (Fin 3 → A)), HPosn p

                There is a position: the left marker.

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

                The interpreted order is linear, from DescriptiveComplexity.tagTupleOrder – no tag-pair case analysis, exactly as for stage 3.

                Dependency graph

                The budget #

                source
                theorem DescriptiveComplexity.horn_budget {n : ℕ} (hn : 1 ≤ n) :
                (2 * n * n + n + 2) * (n + 2) < 16 * n * n * n

                The filler cells alone are enough. One dispatch step, two sweeps per round and clause, one sweep per clause of verification: at most (2n² + n + 2)(n + 2) steps for n elements, while the sixteen filler tags contribute 16n³ positions by themselves.

                Dependency graph
                source
                theorem DescriptiveComplexity.card_le_card_hPosn (A : Type) [LinearOrder A] [Finite A] :
                16 * Nat.card A * Nat.card A * Nat.card A ≤ Nat.card { p : UPTag × (Fin 3 → A) // HPosn p }

                The tape really has that many positions: the filler tuples alone inject into the positions.

                Dependency graph