Application of Hierarchical Hybrid Encodings to Efficient Translation of CSPs to SAT

Solving Constraint Satisfaction Problems (CSPs) through Boolean Satisfiability (SAT) requires suitable encodings for translating CSPs to equivalent SAT instances that can not only be efficiently generated, but also efficiently solved by SAT solvers. In this paper we investigate hierarchical and hybrid encodings, as proposed by Velev, namely a previously studied log-direct encoding, and a new combination, the log-order encoding. Experiments on different domain problems with these hierarchical encodings demonstrate their significant promise in practice. Our experiments show that the log-direct encoding significantly outperforms the direct encoding (typically by one or two orders of magnitude) taking advantage not only of the more concise representation, but also of the better capability of the log-direct encoding to represent interval variables. We also show that the log-order encoding is competitive with the order encoding, although more studies are required to understand the tradeoff between the fewer variables and longer clauses in the former, when expressing complex CSP constraints.