Using SAT Encodings to Derive CSP Value Ordering Heuristics

Abstract

In this paper, we address the issue of designing from SAT new value ordering heuristics for CSP. We show that using the direct and support SAT encodings of CSP instances, such heuristics can be naturally derived from the well-known two-sided Jeroslow-Wang heuristic. These heuristics exploit the bi-directionality of constraint supports to give a more comprehensive picture in terms of domain reduction when a given value is assigned to (resp. removed from) a given variable. Interestingly, in the context of a backtracking search algorithm that exploits binary branching and the adaptive variable ordering heuristic dom/wdeg, we experimentally observed that the new heuristics yielded the best results on satisfiable and unsatisfiable instances when following the promise and the fail-first policies, respectively.