Backjumping is sound

When the search finds a leaf whose certificate ties the incumbent's, it harvests the automorphism autoOf relating the two labellings and then backjumps: it abandons every branch between the current leaf and the deepest node the two leaves share. This file justifies that.

• commonPrefix* — the elementary facts about Canon.commonPrefix, which measures how much of two leaves' paths coincide.
• auto_path — the harvested automorphism follows the paths. If two nodes agree on their first j individualised vertices then autoOf sends the j-th choice of one to the j-th choice of the other. This is where Pinned pays off: Node.pin parks both choices at the same position in the labelling, so autoOf_get reads off the correspondence.
• Node.ancestor — every prefix of a node's path is itself a node.
• jump_sound — the payoff. Let q be the shared depth-j node. Then autoOf fixes q pointwise and maps q's child along path1 to q's child along path2, so the two subtrees have exactly the same set of leaf keys. Everything still to be found under the first is therefore already recorded under the second — the branch depth-first search has finished.

The longest common prefix

theorem IsoGraph.Canon.commonPrefixFrom_ge (a b : Array ℕ) (m fuel i : ℕ) : i ≤ m → i ≤ commonPrefixFrom a b m fuel i

theorem IsoGraph.Canon.commonPrefixFrom_le (a b : Array ℕ) (m fuel i : ℕ) : i ≤ m → commonPrefixFrom a b m fuel i ≤ m

theorem IsoGraph.Canon.commonPrefixFrom_eq (a b : Array ℕ) (m fuel i k : ℕ) : i ≤ k → k < commonPrefixFrom a b m fuel i → a[k]! = b[k]!

theorem IsoGraph.Canon.commonPrefixFrom_ne (a b : Array ℕ) (m fuel i : ℕ) : i ≤ m → m ≤ i + fuel → commonPrefixFrom a b m fuel i < m → a[commonPrefixFrom a b m fuel i]! ≠ b[commonPrefixFrom a b m fuel i]!

theorem IsoGraph.Canon.commonPrefix_le (a b : Array ℕ) : commonPrefix a b ≤ min a.size b.size

theorem IsoGraph.Canon.commonPrefix_eq {a b : Array ℕ} {k : ℕ} (h : k < commonPrefix a b) : a[k]! = b[k]!

theorem IsoGraph.Canon.commonPrefix_ne {a b : Array ℕ} (h : commonPrefix a b < min a.size b.size) : a[commonPrefix a b]! ≠ b[commonPrefix a b]!

theorem IsoGraph.Canon.commonPrefix_take (a b : Array ℕ) : List.take (commonPrefix a b) a.toList = List.take (commonPrefix a b) b.toList

The paths of two leaves agree strictly before their longest common prefix.

The automorphism relating two leaves maps one branch onto the other

theorem IsoGraph.Canon.Part.WF.lab_permArr {n : ℕ} {p : Part} (hp : WF n p) : PermArr n p.lab

theorem IsoGraph.Canon.auto_path {n : ℕ} {f : ℕ → ℕ → Bool} {path1 path2 : Array ℕ} {ip1 ip2 : Array UInt64} {p1 p2 : Part} (h1 : Node n f path1 ip1 p1) (h2 : Node n f path2 ip2 p2) {j : ℕ} (hj1 : j < path1.size) (hj2 : j < path2.size) (hpre : List.take j path1.toList = List.take j path2.toList) : (autoOf n p1.lab p2.lab)[path1[j]!]! = path2[j]!

The harvested automorphism follows the paths. If two nodes agree on their first j individualised vertices, the permutation autoOf builds from their labellings sends the j-th choice of one to the j-th choice of the other — because Node.pin parks both at the same position.

Ancestors

theorem IsoGraph.Canon.Node.ancestor {n : ℕ} {f : ℕ → ℕ → Bool} {path : Array ℕ} {ip : Array UInt64} {p : Part} (h : Node n f path ip p) (j : ℕ) : j ≤ path.size → ∃ (iq : Array UInt64) (q : Part), Node n f (path.extract 0 j) iq q

Every prefix of a node's path is itself a node.

Backjumping is sound

theorem IsoGraph.Canon.jump_sound {n : ℕ} {f : ℕ → ℕ → Bool} {path1 path2 : Array ℕ} {ip1 ip2 iq : Array UInt64} {p1 p2 q : Part} {j : ℕ} {k : List (List UInt64)} (h1 : Node n f path1 ip1 p1) (h2 : Node n f path2 ip2 p2) (hq : Node n f (path1.extract 0 j) iq q) (hcert : certOf (Graph.ofOracle n f) p1.lab = certOf (Graph.ofOracle n f) p2.lab) (hj : j ≤ commonPrefix path1 path2) (hj1 : j < path1.size) (hj2 : j < path2.size) (hreach : Reach n f (childInv (Graph.ofOracle n f) iq q path1[j]!) (child (Graph.ofOracle n f) q path1[j]!).1 k) : Reach n f (childInv (Graph.ofOracle n f) iq q path2[j]!) (child (Graph.ofOracle n f) q path2[j]!).1 k

The key lemma behind the backjump. Two leaves with equal certificates differ by an automorphism γ. If j is the length of their common path prefix and q the depth-j node they share, then γ fixes q and sends q's child path1[j] to q's child path2[j]. So every leaf key still to be found below the first branch already occurs below the second — which is the branch depth-first search has already finished.