In recent years, portfolio approaches to solving SAT problems and CSPs have
become increasingly common. There are also a number of different encodings for
representing CSPs as SAT instances. In this paper, we leverage advances in both
SAT and CSP solving to present a novel hierarchical portfolio-based approach to
CSP solving, which we call Proteus, that does not rely purely on CSP solvers.
Instead, it may decide that it is best to encode a CSP problem instance into
SAT, selecting an appropriate encoding and a corresponding SAT solver. Our
experimental evaluation used an instance of Proteus that involved four CSP
solvers, three SAT encodings, and six SAT solvers, evaluated on the most
challenging problem instances from the CSP solver competitions, involving
global and intensional constraints. We show that significant performance
improvements can be achieved by Proteus obtained by exploiting alternative
view-points and solvers for combinatorial problem-solving.

该论文提出了一种名为 Proteus 的分层组合策略解决 CSP 问题的方法，该方法能够将 CSP 实例编码为 SAT 形式，并选择合适的编码和相应的 SAT 求解器进行求解，实验结果表明 Proteus 能够显著提高组合问题求解性能。