Timestamped incidence DAGs for edge CSPs

This is Definition 32 of [KKR18], arXiv:1602.03124v6, printed pp. 15–16. Constraint nodes are original positions paired with timestamps; relation symbols never identify nodes. Arcs retain actual ordered occurrences. Separate finite node supports retain isolated variables, including forest roots.

DAG.IsFDAG contains all six conditions of the definition. Actual incidence is built into DAG.Arc; supported checks its endpoints. unique prohibits reuse of an original incidence at any orientation or time. indegree bounds variable indegree. ordered requires distinct constraint timestamps and a compatible finite topological numbering. Numberings may tie at unrelated nodes: on the finite support these ties can be broken to obtain the source's total order. Conversely a finite total order can be numbered. orderRelation explicitly adds the timestamp comparisons, and ordered_iff_acyclic relates the numbering to the existing acyclic relation API. Local feasibility and the full same-original-constraint no-shortcut condition are feasible and noShortcut.

Condition 5 flips two singleton coordinates successively. Equal ports therefore cancel, as in the paper; they do not become a one-coordinate set flip. Since the base labeling is valid and both ports belong to the same constraint, global validity of this move is equivalent to feasibility of that constraint's tuple.

Main results

• DAG.IsFDAG.subgraph: Observation 33, including isolated nodes.
• DAG.IsFDAG.acyclic: the directed incidence graph is acyclic.
• DAG.Ordered.exists_injective_numbering: a checked finite tie-breaking justification of the source's total-order formulation, including isolated nodes.

No construction of Algorithm 1's forest, improving comparison labeling, or solver is assumed.

@[reducible, inline]

abbrev Cslib.Logic.PL.CSP.DAG.Copy {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Type

An original constraint position paired with its copy's timestamp.

@[reducible, inline]

abbrev Cslib.Logic.PL.CSP.DAG.Node {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Type u_2

Variable nodes and timestamped copies of positional constraints.

structure Cslib.Logic.PL.CSP.DAG.Arc {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Type

An indexed incidence, its timestamp, and its orientation (true means variable to copy).

• occurrence : F.Occurrence

  Original constraint and ordered argument position of this incidence.

• time : ℕ

  Timestamp identifying the copied constraint endpoint.

• incoming : Bool

  true orients the incidence from its variable toward its constraint copy.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.DAG.instDecidableEqArc {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : DecidableEq (Arc F)

def Cslib.Logic.PL.CSP.DAG.Arc.copy {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (a : Arc F) : Copy F

The constraint-copy endpoint of an arc.

def Cslib.Logic.PL.CSP.DAG.Arc.source {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (a : Arc F) : Node F

Source node of an oriented incidence.

def Cslib.Logic.PL.CSP.DAG.Arc.target {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (a : Arc F) : Node F

Target node of an oriented incidence.

def Cslib.Logic.PL.CSP.DAG.pairFlip {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) (o p : F.Occurrence) : F.OccurrenceLabeling Bool

Two individual flips, with cancellation when the occurrences are equal.

@[simp]

theorem Cslib.Logic.PL.CSP.DAG.pairFlip_self {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) (o : F.Occurrence) : pairFlip f o o = f

theorem Cslib.Logic.PL.CSP.DAG.pairFlip_eq {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (f : F.OccurrenceLabeling Bool) {o p : F.Occurrence} (h : o ≠ p) : pairFlip f o p = BitString.flipOn {o, p} f

For distinct occurrences the cancelling pair operation is the usual set flip.

structure Cslib.Logic.PL.CSP.DAG {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Type u_2

A finite directed incidence graph with explicit support for isolated nodes.

• vars : Finset V

  Supported actual variables, retaining isolated roots.

• copies : Finset (Copy F)

  Supported positional constraint copies, retaining isolated copies.

• arcs : Finset (Arc F)

  Used original incidences with their timestamps and orientations.

def Cslib.Logic.PL.CSP.DAG.nodes {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) : Finset (Node F)

All explicitly supported nodes, including isolated roots and constraint copies.

def Cslib.Logic.PL.CSP.DAG.edge {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) (x y : Node F) : Prop

The directed incidence relation, without the auxiliary timestamp comparisons.

def Cslib.Logic.PL.CSP.DAG.orderRelation {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) (x y : Node F) : Prop

Arcs together with all forward timestamp comparisons between supported constraint copies.

def Cslib.Logic.PL.CSP.DAG.Supported {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) : Prop

Every arc has its actual variable and copy in the declared node supports.

def Cslib.Logic.PL.CSP.DAG.Ordered {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (T : F.DAG) : Prop

Timestamp-compatible topological order, encoded by a finite rank witness.

structure Cslib.Logic.PL.CSP.DAG.IsFDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (T : F.DAG) : Prop

All six invariant conditions in KKR Definition 32, with base validity explicit.

• valid : ValidLabeling sem f

  The reference labeling satisfies every original positional constraint.

• supported : T.Supported

  Condition 1: every indexed arc has both endpoints in the support.

• unique (a : Arc F) : a ∈ T.arcs → ∀ b ∈ T.arcs, a.occurrence = b.occurrence → a = b

  Condition 2: an original incidence is used at most once, in one orientation and copy.

• indegree (a : Arc F) : a ∈ T.arcs → ∀ b ∈ T.arcs, a.incoming = false → b.incoming = false → a.occurrence.var = b.occurrence.var → a = b

  Condition 3: a variable has at most one incoming arc.

• ordered : T.Ordered

  Condition 4: timestamps are globally distinct and extend to a topological order.

• feasible (a : Arc F) : a ∈ T.arcs → ∀ b ∈ T.arcs, a.incoming = true → a.copy = b.copy → ValidLabeling sem (pairFlip f a.occurrence b.occurrence)

  Condition 5: an incoming port exchanges feasibly with any port at its copy.

• noShortcut (a : Arc F) : a ∈ T.arcs → ∀ b ∈ T.arcs, a.incoming = true → a.occurrence.fst = b.occurrence.fst → a.time < b.time → ¬ValidLabeling sem (pairFlip f a.occurrence b.occurrence)

  Condition 6: an old incoming port cannot exchange with a later-used port of the same original constraint.

def Cslib.Logic.PL.CSP.DAG.Subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (S T : F.DAG) : Prop

Subgraph inclusion permits deletion of isolated nodes as well as arcs.

theorem Cslib.Logic.PL.CSP.DAG.IsFDAG.subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {S T : F.DAG} (h : IsFDAG sem f T) (hst : S.Subgraph T) (hs : S.Supported) : IsFDAG sem f S

Observation 33: every supported subgraph inherits all six conditions.

def Cslib.Logic.PL.CSP.DAG.restrict {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (T : F.DAG) (vs : Finset V) (cs : Finset (Copy F)) : F.DAG

Restrict to selected variable and copy supports, retaining precisely the arcs between them.

theorem Cslib.Logic.PL.CSP.DAG.restrict_subgraph {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (T : F.DAG) (vs : Finset V) (cs : Finset (Copy F)) : (T.restrict vs cs).Subgraph T

Restriction deletes nodes and arcs.

theorem Cslib.Logic.PL.CSP.DAG.Supported.restrict {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {T : F.DAG} (h : T.Supported) (vs : Finset V) (cs : Finset (Copy F)) : (T.restrict vs cs).Supported

Restriction retains the endpoint-support condition.

theorem Cslib.Logic.PL.CSP.DAG.IsFDAG.restrict {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} (h : IsFDAG sem f T) (vs : Finset V) (cs : Finset (Copy F)) : IsFDAG sem f (T.restrict vs cs)

Observation 33 specialized to an executable induced restriction.

theorem Cslib.Logic.PL.CSP.DAG.isFDAG_empty {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} (hf : ValidLabeling sem f) : IsFDAG sem f { vars := ∅, copies := ∅, arcs := ∅ }

The empty graph (with no nodes) is an f-DAG for every valid labeling.

theorem Cslib.Logic.PL.CSP.DAG.IsFDAG.acyclic {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {sem : Rel → List Bool → Bool} {f : F.OccurrenceLabeling Bool} {T : F.DAG} (h : IsFDAG sem f T) : Relation.Acyclic T.edge

A compatible rank excludes all directed cycles.

theorem Cslib.Logic.PL.CSP.DAG.Supported.orderRelation {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} (h : T.Supported) {x y : Node F} (hxy : T.orderRelation x y) : x ∈ T.nodes ∧ y ∈ T.nodes

Supported arcs and timestamp comparisons remain inside the finite node support.

theorem Cslib.Logic.PL.CSP.DAG.ordered_iff_acyclic {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} (h : T.Supported) : T.Ordered ↔ (∀ c ∈ T.copies, ∀ d ∈ T.copies, c.2 = d.2 → c = d) ∧ Relation.Acyclic T.orderRelation

The rank formulation is equivalent to acyclicity after adding the timestamp order. This uses the existing finite topological-numbering theorem rather than a separate DAG API.

theorem Cslib.Logic.PL.CSP.DAG.Ordered.exists_injective_numbering {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} {T : F.DAG} (h : T.Ordered) : ∃ (number : ↥T.nodes ↪ ℕ), ∀ (x y : ↥T.nodes), T.orderRelation ↑x ↑y → number x < number y

Break rank ties on the finite support without changing any required strict comparison. The resulting injective natural numbering induces the source's strict total order on supported nodes. This also accounts for isolated nodes, whose original ranks may all have been equal.