Documentation

CslibFrontier.Computability.Complexity.Problems.CSP.RotationSystem

Cyclic argument order in CSP incidence rotations #

Each argument occurrence determines two distinct indexed ends of its incidence edge. The constraint-side rotation must follow the scope's cyclic argument order. Variable-side rotations are unrestricted beyond the graph rotation-system contract. Repeated variables and identical constraints keep their different argument/constraint positions. Nullary constraints have no argument darts, so the order condition is vacuous for them.

This is the argument-order part of the incidence model in Fulla–Živný, On Planar Valued CSPs, arXiv:1602.06323v3, Section 2.1. It is not a genus-zero condition, planarity recognizer, supplied embedding reduction or full planar CSP definition.

Main definitions #

source
def Cslib.Complexity.CSP.incidenceDart {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) (side : Bool) :
(incidenceGraph F).Dart

A chosen end of an argument's incidence edge; true is its constraint end.

Instances For
    source
    theorem Cslib.Complexity.CSP.incidenceDart_injective {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (side : Bool) :
    Function.Injective fun (o : F.Occurrence) => incidenceDart o side

    Occurrence identity is retained at each choice of edge end.

    source
    theorem Cslib.Complexity.CSP.incidenceDart_true_ne_false {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o p : F.Occurrence) :
    incidenceDart o true ≠ incidenceDart p false

    Constraint-side and variable-side indexed ends remain distinct, even at repeated names.

    source
    @[simp]
    theorem Cslib.Complexity.CSP.vertex_incidenceDart {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) (side : Bool) :
    (incidenceDart o side).vertex = if side = true then F.numVars + ↑o.fst else List.idxOf o.var F.distinctVars

    The endpoint agrees with the original incidence construction.

    source
    theorem Cslib.Complexity.CSP.exists_incidenceDart {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (d : (incidenceGraph F).Dart) :
    ∃ (o : F.Occurrence), incidenceDart o d.2 = d

    Every indexed edge end comes from exactly one argument and its endpoint choice.

    source
    def Cslib.Complexity.CSP.argumentSuccessor {Rel V : Type} {F : Logic.PL.CSP Rel V} (o : F.Occurrence) :
    F.Occurrence

    Next position in the same scope, with last-to-first wraparound.

    Instances For
      source
      @[simp]
      theorem Cslib.Complexity.CSP.argumentSuccessor_constraint {Rel V : Type} {F : Logic.PL.CSP Rel V} (o : F.Occurrence) :
      (argumentSuccessor o).fst = o.fst

      The next argument belongs to the same constraint position.

      source
      theorem Cslib.Complexity.CSP.argumentSuccessor_injective {Rel V : Type} {F : Logic.PL.CSP Rel V} :
      Function.Injective argumentSuccessor

      The scope's cyclic permutation makes argument succession injective.

      source
      def Cslib.Complexity.CSP.RespectsArgumentOrder {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) :
      Prop

      The cyclic rotation at every constraint follows its ordered argument positions. Rotations at variable vertices are governed only by the graph rotation-system contract.

      Instances For