Chronological edge-CSP forest search

The executable forest-growing part of Algorithm 1, steps 1–5, of [KKR18], arXiv:1602.03124v6, printed p. 10. A run stops at exhaustion, augmentation, or the first blossom; contraction and recursive solving are separate. The input is the existing positional CSP, Boolean occurrence labeling and relation evaluator. Variable names need only decidable equality. No finite universe of variable names is scanned.

Expansion records are stored newest first. An expansion's timestamp is the number of older records, starting at zero rather than the paper's one. The scan order is constraint position then port position. Each newly added variable records its actual parent ports, so ancestry reconstruction is executable structural recursion through older records. The search itself recurses on the remaining incidence list: every continuation removes its chosen input port.

Step 4b compares the original constraint position, not the copied node. Meeting data retain the partially expanded copy, both ancestral paths and the meeting ports. Meeting.prunedDAG removes all outgoing arcs at that copy before inserting the second incoming arc, as required by Lemma 34's moreover clause (printed p. 16).

This module defines the executable search and elementary scan/termination properties. The mathematical correctness of its returned events and exhaustion requires separate proofs.

Main definitions

• search: total deterministic forest-growing search.
• Meeting.prunedDAG: the terminal graph required by Lemma 34's moreover clause.
• Log.ancestry: actual parent-port reconstruction through older expansions.

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

One chronological expansion: its input port and the children discovered during its scan. The original constraint is the input port's constraint position.

• input : F.Occurrence

  Actual unused incidence selected in step 2.

• outputs : List F.Occurrence

  Actual output ports inserted by step 4a, in scan order.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Forest.instDecidableEqExpansion {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : DecidableEq (Expansion F)

@[reducible, inline]

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

Expansion records in reverse chronological order. Timestamps count older records.

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

The ports and timestamp witnessing one variable's discovery.

• input : F.Occurrence

  Port of the already visited variable that expanded this copied constraint.

• output : F.Occurrence

  Port of the newly discovered variable.

• time : ℕ

  Number of expansions preceding discovery.

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

A root path together with its copied constraint timestamps, in traversal order. The mathematical walk is the library's existing Walk.

• walk : F.Walk

  The root-to-variable walk, forgetting timestamps.

• times : List ℕ

  One copy timestamp per step of the walk.

def Cslib.Logic.PL.CSP.Forest.Log.used {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : Log F → List F.Occurrence

Used positional ports, independent of their orientation and copy.

def Cslib.Logic.PL.CSP.Forest.Log.children {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : Log F → List V

Variables discovered by step 4a, with discovery order irrelevant to membership.

def Cslib.Logic.PL.CSP.Forest.Log.parent? {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] : Log F → V → Option (Parent F)

Actual parent ports of a visited nonroot variable, found without choosing a witness.

def Cslib.Logic.PL.CSP.Forest.Log.ancestry {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] : Log F → V → Ancestry F

Follow parents through strictly older expansion records. An undiscovered variable has the length-zero path at itself; on a search event both requested variables are visited.

def Cslib.Logic.PL.CSP.Forest.Log.arcs {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : Log F → List (DAG.Arc F)

Chronological arcs of the recorded expansions, with actual positional incidences.

def Cslib.Logic.PL.CSP.Forest.Log.toDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (roots : List V) (es : Log F) : F.DAG

Convert the executable log to the existing finite incidence DAG, retaining isolated roots. This is a representation conversion, not an invariant assertion.

def Cslib.Logic.PL.CSP.Forest.Log.Visited {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (roots : List V) (es : Log F) (v : V) : Prop

A variable is visited if it is a root or was discovered as an output.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Forest.Log.instDecidableVisited {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (roots : List V) (es : Log F) (v : V) : Decidable (Visited roots es v)

def Cslib.Logic.PL.CSP.Forest.Log.SameParent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) (i : Fin (List.length F)) : Prop

Step 4b: the variable's predecessor is a copy of the same original constraint. The timestamp of that predecessor need not be the current timestamp.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Forest.Log.instDecidableSameParent {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) (i : Fin (List.length F)) : Decidable (es.SameParent v i)

theorem Cslib.Logic.PL.CSP.Forest.Log.ancestry_length {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) : (es.ancestry v).times.length = (es.ancestry v).walk.steps.length

Timestamps along every reconstructed ancestry have exactly one entry per walk step.

theorem Cslib.Logic.PL.CSP.Forest.Log.ancestry_length_le {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) : (es.ancestry v).walk.steps.length ≤ List.length es

Every reconstructed ancestry has length at most the number of expansions.

theorem Cslib.Logic.PL.CSP.Forest.Log.ancestry_time_lt {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (es : Log F) (v : V) {t : ℕ} (ht : t ∈ (es.ancestry v).times) : t < List.length es

Every copy along a reconstructed ancestral path strictly predates the next expansion.

def Cslib.Logic.PL.CSP.Forest.roots {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (f : F.OccurrenceLabeling Bool) : List V

Inconsistent roots in positional incidence order, without a finite variable universe.

@[simp]

theorem Cslib.Logic.PL.CSP.Forest.mem_roots {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (f : F.OccurrenceLabeling Bool) (v : V) : v ∈ roots f ↔ Inconsistent f v

Every inconsistent variable, and only an inconsistent variable, is an initial root.

def Cslib.Logic.PL.CSP.Forest.partners {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (a : F.Occurrence) : List F.Occurrence

The distinct same-constraint partners whose two-port flip is valid, in positional order. Testing global validity is equivalent to the source's local test when the base is valid.

@[simp]

theorem Cslib.Logic.PL.CSP.Forest.mem_partners {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (a b : F.Occurrence) : b ∈ partners sem f a ↔ a.fst = b.fst ∧ a.var ≠ b.var ∧ ValidLabeling sem (DAG.pairFlip f a b)

Exact feasible-partner scan specification.

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

Terminal scan data before augmentation or contraction. Both ancestry walks and their timestamps are retained, including shared copied constraints.

• roots : List V

  Inconsistent variables initially inserted as isolated roots.

• older : Log F

  Completed older expansions, newest first.

• current : Expansion F

  Current expansion up to, but excluding, the meeting output.

• output : F.Occurrence

  Feasible output already visited, with no predecessor at this original constraint.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Forest.instDecidableEqMeeting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] : DecidableEq (Meeting F)

def Cslib.Logic.PL.CSP.Forest.Meeting.left {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : Ancestry F

Root-to-input ancestry before inserting the current copy.

def Cslib.Logic.PL.CSP.Forest.Meeting.right {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : Ancestry F

Root-to-output ancestry before inserting the current copy. Step 4b ensures a terminal output was not newly discovered at the current copy.

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

Terminal copied constraint and its actual chronological timestamp.

def Cslib.Logic.PL.CSP.Forest.Meeting.toDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : F.DAG

The forest at the instant the feasible already-visited output is encountered.

def Cslib.Logic.PL.CSP.Forest.Meeting.prunedDAG {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : F.DAG

Lemma 34's terminal graph: prune all current-copy children and add the meeting incoming arc. Newly discovered variables remain supported as isolated nodes.

def Cslib.Logic.PL.CSP.Forest.Meeting.walk {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : F.Walk

Candidate augmentation from step 4c: left ancestry, the two meeting ports, reversed right ancestry. Its validity needs the meeting-DAG argument, not reversal of an arbitrary f-walk.

inductive Cslib.Logic.PL.CSP.Forest.ScanResult {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Type

Result of one complete feasible-partner scan.

• continued {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (outputs : List F.Occurrence) : ScanResult F

  All feasible partners were either inserted or skipped by source step 4b.

• meeting {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (outputs : List F.Occurrence) (output : F.Occurrence) : ScanResult F

  First previously visited partner that is not skipped by source step 4b.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Forest.instDecidableEqScanResult {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} : DecidableEq (ScanResult F)

def Cslib.Logic.PL.CSP.Forest.scan {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (roots : List V) (older : Log F) (input : F.Occurrence) : List F.Occurrence → List F.Occurrence → ScanResult F

Scan step 4 in positional order. outputs contains the children already inserted at this copy; they participate in both the visited and same-original-parent tests.

inductive Cslib.Logic.PL.CSP.Forest.Result {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Type u_2

A forest-growing run stops at exhaustion or the first augmentation/blossom event. The event retains actual ancestor paths and positional local data for the contraction layer.

• exhausted {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (log : Log F) : Result F

  There is no unused incidence at any visited variable.

• augment {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (meeting : Meeting F) : Result F

  First meeting between different rooted trees.

• blossom {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (meeting : Meeting F) : Result F

  First meeting within one rooted tree.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.Forest.instDecidableEqResult {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] : DecidableEq (Result F)

@[irreducible]

def Cslib.Logic.PL.CSP.Forest.run {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) (rs : List V) (es : Log F) (remaining : List F.Occurrence) : Result F

Run steps 2–5. The remaining incidence list is the termination measure; each continuation erases the selected input, regardless of any newly discovered children. The final filter only removes additional used ports. No unbounded fresh timestamp or variable-label scan is used.

def Cslib.Logic.PL.CSP.Forest.search {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (sem : Rel → List Bool → Bool) (f : F.OccurrenceLabeling Bool) : Result F

Fresh Algorithm 1 forest search. Preconditions about edge instances, validity and even delta-matroids belong to correctness theorems; the program itself is total on arbitrary CSPs.