Search Strategy Simulation in Constraint Booleanization

better solution methods. In other words, the goal in this case is not necessarily to devise a Booleanization that will outperform native methods for constraints of type X, but rather one whose effectiveness is maximized, particularly by capitalizing on successful techniques used in native methods. It is in this spirit that we propose, in this work, a new, substantially improved Boolean encoding of C UMULATIVE, one of the the most widely used global constraints (Rossi, van Beek, and Walsh 2006). We first present an encoding that utilizes recent advances in solving pseudo-Boolean (PB) constraints (Eén and Sörensson 2006), and then show how we can augment the encoding to effectively simulate domain splitting, a search strategy known to be beneficial for C U MULATIVE constraints in native search algorithms (Simonis and O’Sullivan 2008; Huang and Korf 2009). Empirical results indicate that our new encoding leads to significant improvements over the original Booleanization, while we observe, on the other hand, the efficiency of native solvers over our Booleanization on some of the benchmarks. In concluding the paper, we discuss analytically some strength and weaknesses of our work. Within the recently proposed Universal Booleanization framework, we consider the C UMULATIVE constraint, for which the original Boolean encoding proves ineffective, and present a new Boolean encoding that causes the SAT solver to simulate, largely, the search strategy used by some of the best-performing native methods. Apart from providing motivation for future research in a similar direction, we obtain a significantly enhanced version of Universal Booleanization for problems containing C UMULATIVE constraints.

Authors

• Jinbo Huang NICTA and Australian National University

Keywords

No keywords are indexed for this paper.