backjumping

variant of backtracking

cut some search

backtracking

conceptually:

• choose a variable x
• for each value v in the domain of x:
  • add the constraint x = v
  • recursively solve the problem
  • remove the constraint x = v

backtracking with partial assigment

instead of adding x = v, keep a partial assigment
set of assigments to variables, some variables unassigned

initially: all variables unassigned

• if a constraint is violated by the partial assigment
  • return unsat
• if the partial assigment satisfies all constraints
  • return sat
• choose a variable x
• for each value v in the domain of x:
  • add x = v the partial assigment
  • recursively solve the problem

tree of recursive calls

nodes: recursive calls of the algorithm

edges: assigments x = v
for each assigment there is a new recursive call (node)

tree of recursive calls: examples

note: different variables at the same level
example: y on one side, z in the other

nodes are recursive calls

in each recursive call (each node), some assigments x = v
each assigment ⇒ new recursive call (node at the end of the edge)

• root: main call
• variable chosen in the root: x
• therefore: number of recursive calls:
  • first with x=1
  • second with x=2
  • third with x=3

assigment made in a node ⇒ take effect in the child

the crosses

X means: partial assigment violates one or more constraints

1. all variables in the scope of the constraint are assigned
2. their values are not a tuple in the relation of the constraint

algorithm comes back

violated constraints: example

assigment x=1, y=0

constraints: x < y, x > y, x < z

which of these are satisfied or violated?

violated constraint: answer

assigment x=1, y=0

x<y

variables x and y
both assigned
values do not satisfy the constraint ⇒ violated

x>y

variables x and y
both assigned
values satisfy the constraint ⇒ satisfied

x<z

variables x and z;
z not assigned (does not have a value)
variable not assigned ⇒ not satisfied, not violated

when to stop

assignment satisfies all constraints

when looking for all satisfying assigments: go ahead until all values are considered

backjumping

some variables may be avoided:

if everything remains the same
(same subtrees from T1 and T2)
then, skip T3

only if everything stays the same!

how much is saved?

subtree from T3 may be exponentially large

how to detect that skipping it is possible?

how to check that skipping is possible?

just check with node skipped:
requires checking subtrees rooted in T1 and T2 again
just to save searching from T3

instead: check it when searching in T1 and T2 the first time

when is skipping correct?

assignment y = b still added

skipped: assigments for w
jump straight to assigments for z

correct if: nothing changes in T1 and T2 removing w = d

what could change?

skipping is correct if: nothing changes when removing w = d

what changes with this removal?

inconsistency with w = d (cross)
consistency without w = d (no cross)

violated constraint has w in the scope

cannot skip w = d
something changes by removing this assigment

why the name "backjumping"?

when going down: set w = d as usual

when coming back, check whether w = d was necessary
if not, skip the node (jump when coming back)

as if the node was skipped when going down
actually done when coming back

backjumping: leaves

simplest case: inconsistency in all leaves

after w = 2, should try with w = 3
do not if inconsistency in leaves do not require w = 2

same if y = 1 is not necessary

values of the other variables …x,z violate some constraints ⇒ value of y,w not necessary

skip trying other values of y and w

as if choosing x = 1 and then iterating over the values of z

inconsistency in the leaves

inconsistency is enough for backtracking
not enough for backjumping

• check whether the values of …x,y,w violate some constraints for all values of z
• if so, check whether the values of …x,y violate some constraints for all values of z
• if so, check whether the values of …x violate some constraints for all values of z
• …

no longer inconsistent ⇒ jump there

inconsistency in the leaves: improvement

required consistency checks:

stop when partial assigment no longer violate constraints

sort assigments on values of z:

same assigments, different order

allows checking in the leaves

inconsistency checks in the leaves

when in the leaf for z = 1
can check consistency of:

return the shortest assignment that still violates some constraint

same for the leaves z=2 and z=3

combining

from each leave: shortest falsifying assignment

example:

z = 1: …,x,y
z = 2: …,x
z = 3: …,x,y

meaning:

with z = 1, values of …,x,y necessary for inconsistency (w is not)
with z = 2, values of …,x necessary for inconsistency (y and w are not)
with z = 3, values of …,x,y necessary for inconsistency (w is not)

result: w is unnecessary in all
instead, y is necessary in some

skip w
do not skip y (otherwise, cross in z=2 disappears)

algorithm

when reaching inconsistency in a node:

• try shortening the partial assigment
• stop when it becomes consistent
• the last variable of the partial assigment
  (last = lowest in the branch)

when coming back from leaves:

• collect all of these “last variables”
• go straight to the lowest of them

internal nodes

backjumping may still be possible

backjumping possible if:

values in the branch P unncessary for inconsistency of the leaves of T2

not always the case!

backjumping internal nodes

backjumping possible if:

values in the branch P unncessary for inconsistency of the leaves of T2

path P+Q ends up in inconsistency
same should be for J+Q

same for P+R and J+R

what to check

when reaching inconsistency (leaf):
remove from assigment as many variables as possible
start trying to remove the last assigned variables
do not stop at the first necessary one

a,b,c,d,e,f,g,x,y,w,z inconsistent (by assumption)
a,b,c,d,e,f,g,x,y,w   consistent: restore z
a,b,c,d,e,f,g,x,y,z   inconsistent: remove w
a,b,c,d,e,f,g,x,z     inconsistent: remove y
a,b,c,d,e,f,g,z       consistent: restore x
a,b,c,d,e,f,x,z       consistent: restore g
a,b,c,d,e,g,z         inconsistent: remove f

remove variable from assignment
still inconsistent ⇒ remove variable
proceed with previous

result: a minimal partial assigment falsifying some constraints

parent of leaves

each leaf returns a list of variables:
these are sufficient for inconsistency

parent of them: do the same
return a list of variables that are sufficient for inconsistency

how:
variables sufficient for all chidren are sufficient for their parent

return the union of these lists of variables

the partial assignment on these variables guarantees inconsistency in all leaves

internal nodes

invariant: every node returns a list of variables
these are sufficient for reaching inconsistency in all leaves

each child returns this list for its leaves
parent must return this list for all leaves of all its children

parent returns the union

example

values omitted

the three crossed nodes return:

• p,y,w,z
• p,x,u,z
• x,y,w

node M merges the first two and returns the result

this result is merged with the third set in node N,
obtaining p,x,y,u,w,z

variables w and z are below N
the others are p,x,y,u

implies that u is the highest variable that guarantees inconsistency in all nodes below N
backjump to the node over u

variant

when merging the sets from the children in a node
remove all variables assigned below the node

why: set is used to jump over the node
not below
variables below are irrelevant

invariant in a node

every node returns the variables that guarantee the inconsistency of all leaves in its subtree

a node receives such sets from all its children

to maintain the invariant true:
combine them to return the variables that guarantee the inconsistency in all leaves in its subtree

if this condition is kept true:
this set of variables tells where to backjump

set of variables, formally

for each node: a set of variables that guarantees the inconsistency in all its descendant leaves

leaf:

remove variables, check if assignment still violates constraints

internal node:

if the sets of variables of the chidren are correct
their union is a correct set of variables for the node

by recursive induction: set is correct for all nodes

algorithm for finding the set

in the leaves (nodes where inconsistency is detected):

• remove last variable from the assignment if what result is still inconsistent
• remove second-last variable from the assignment if what result is still inconsistent
• …

in each internal node:

• merge sets from the chidren
• remove the variables of the node
• send result to the parent

why removing the variable chosen in the node?

set is used for jumping up as much as possible

only variables above the node in the tree count

variable is in the node, not above it

use of the set

set of variables that guarantee inconsistency in all descendant leaves of the node

other variables not necessary

example: variables in the path from the root to the node are a,b,c,d,e,f,g
set in the node is a,d,e

variables f,g unnecessary
do not try other values for them
skip the nodes where they have been chosen

summary

like backtracking, but:

• in the leaves (where the partial assigment violates some constraints), try removing variables starting from the last; if that makes all constraints satisfied, put the variable back in
• every node receive one such set of variables from the chidren; it merges them and removed the variables that is assigned to all possible values in the node; this set is returned to its parent, but
• instead of the parent, go back to the lowest node in the path from the root to the node where the variable is in the returned set

double jump

from c, jump to a
what to do in a?

do as if c were a (direct) child of a

receive the set of variables from c,
merge with that from the other child, etc.

the skipped nodes do not exist

ignore the nodes in the shaded area

as if they never existed

behave as if c were the second child of a

set of variables in the leaves

partial assigment falsifies a constraint with scope ⟨x,y⟩ and a constraint with scop ⟨x,z⟩

therefore: inconsistency remains removing y alone
but also removing z alone

return which set of variable?

both {x,y} and {x,z} are correct
both sets produces inconsistency

choice of the set in the leaves

inconsistent = violated constraint(s)

scope of a violated constraint ⇒ minimal assigment falsifying that contraint

(may not be minimal: another constraint may bave a proper subset as the scope)

choice of variables: scope of a violated constraint

what if more than one constraint is violated?
choose which constraint?

choice of violated constraint

higher jump ⇒ skip more nodes

prefer the constraint allowing for the highest jump

constraint whose lowest variable is highest in the tree

technically:

• for each violated constraint, select the variable lowest in the tree
• compare the selected variables of each constraint, take the one that is highest in the tree
• the set is the scope of the constraint of that variable
  (ties: look the second-lowest variables, etc.)

a different method

based on the primal graph

requirement:

replacing P with J,
the inconsistencies at the bottom of Q, R, etc. do not change

if the variables chosen in Q, R, etc. are not in any constraint with the variables in P, then P can be skipped

algorithm

in every node:

• select all variables above the node that are not in a constraint with the variable of the node
• return this set to the parent
• the parent merges these sets, remove the variable in the node and sends the result to its parent