St Andrews Algorithm
Ian Gent & Andrew Rowley, unpublished
Based on a least commitment principle
- we donít want to set universal variables if possibleÖ
- Ö so we donít set them at all
Search still proceeds outside in Ö
Ö but we just leave a place holder for universals
When no existential variables left, set universals
- by a magic call to g.o.f. Davis Putnam
On backtracking set universal variables in solutions
- backjump over others as in SBJ