Order of variables for couplings

jgraley commented 2 years ago

It's fair to say that:

Backjumping is "defeated" by couplings (see comment)
But it's likely that:
- most couplings are tight because they are identifier couplings
- reverse traversal from leaf toward root is fast because fewer options due tree topology
Therefore, variable ordering "residual" paths should be reversed
Do a forward walk until non-trivial coupling is encountered, then for each residual, reverse-walk until an already-seen node is discovered. Then resume forward.
- But also deal with branching during the backward walk, presumably by going forward again on the branch.
- Probably ends up as a forward-backward-forward-backward-... recursion structure

jgraley commented 2 years ago

Likely to need "Equivalence solves to category-result" from #507 before the performance benefit shows up. Done

jgraley commented 2 years ago

Explanation of backjumping is "defeated" by couplings.

First note

it is OK to discuss the problem topology as defined by the agents even though we "munge up" their constraints. This is because we don't munge up the variables, and at least as far as back-jumping is concerned, it's the variable ordering that drives everything. Also the constraint munging only locally affects the inter-dependencies of variables.

No couplings case

Trees tend to have branches. Imagine a tree with no couplings and root path X0..Xp, branch from Xp of Y0 to Yq and another from Xp of Z0..Zr. The depth-first walk order here is X0..Xp, Y0..Yq, Z0..Zr. It "flattens" the whole tree, making Yq and Z0 neighbours even though they don't share any constraints.

A naive backtracker will cross the Y and Z branches => slow.

Graph-based back-jumping will progress from X0 to Xp to Y0 to Yq and then to Z0 onward. If it hits a dead end it will back-step to Z0 because all the Z's share constraints. But after Z0 it will jump past all the Y's because it has no constraint with them, and jump back to Xp. This avoids repeating the Y branch. If this were all that happened, the complexity would be size(X)*Nbranches i.e. for each branch, search is just a walk of the tree. This comes from the tight adherence to the (true) tree structure in this case.

Back-jumping can uncross the Y and Z branches for a speedup => fast.

Coupling case

To the example tree, add that Yq and Zr are coupled (arrow-head model means they remain separate variables but now have a coupling constraint between them).

As before we progress from X0 to Xp to Y0 to Yq and then to Z0 onward. Suppose we hit dead end at Zr i.e. fail on the coupling constraint. We step back to Z0. In this case, all the Z's are in "trouble" and we must not backjump past any variable that could "fix" any of the Z's. This includes Zr which is in constraint with Yq. We have to backstep from Z0 to Yq and in fact the whole situation has reverted to that of backtracking.

Not safe to uncross Y and Z; backjumping "sees" this and re-crosses them => slow.

How to fix

Build the variable ordering with the Z's reversed, i.e. X0..Xp, Y0..Yq, Zr..Z0. Note that Yq and Zr, which are coupled, are now neighbours.

Assume we get to Yq, at the expected cost (a whole tree walk). Zr can now be restricted by the coupling constraint to (hopefully) a small set of candidates[1]. As we work through from Zr back to Z0, we progress from child to parent which limits candidates to just one (the parent), or a much reduced set in the case of Stuff nodes (the ancestors). So we should be able to check the Z's very rapidly.

Y and Z branches are still crossed, but Z is fast thanks to (a) general graph topology and (b) propagation through coupling constraint => fast-ish.

Subtle correction

Actually if Xp is a Disjunction, there is a 3-constraint tying Y0 and Z0. Similarly if Y0 and Z0 are neighbours in a sequence, there will be a 2-constraint between them (other constraints will tie them to Xp). However I think the argument stands and the fix is the same. It's just that in the non-coupling case, the jump might be to Y0 rather than Xp.

[1]

Might be best to constrain coupled variables like Zr from its own root Z0 with a descendent-of constraint and then use https://github.com/jgraley/inferno-cpp2v/issues/510#issuecomment-1104844748 to get efficient reduction of candidates

jgraley / inferno-cpp2v