We investigate the use of value ordering in backtracking search for Quantified Constraint Satisfaction problems (QCSPs). We
consider two approaches for ordering heuristics. The first approach is solution-focused and is inspired by adversarial search:
on existential variables we prefer values that maximise the chances of leading to a solution, while on universal variables
we prefer values that minimise those chances. The second approach is verification-focused, where we prefer values that are
easier to verify whether or not they lead to a solution. In particular, we give instantiations of this approach using QCSP-Solve’s
pure-value rule Gent et al. (QCSP-solve: A solver for quantified constraint satisfaction problems. In
Proceedings of IJCAI, pp. 138–143,
2005). We show that on dense 3-block problems, using QCSP-Solve, the solution-focused adversarial heuristics are up to 50% faster
than lexicographic ordering, while on sparse loose interleaved problems, the verification-focused pure-value heuristics are
up to 50% faster. Both types are up to 50% faster on dense interleaved problems, with one pure-value heuristic approaching
an order of magnitude improvement.
Keywords Value ordering - Quantified CSPs - Backtracking search
This work was supported in part by Microsoft Research through the European PhD Scholarship Programme, and by the Embark Initiative
of the Irish Research Council for Science, Engineering and Technology (IRCSET).