CP-SAT 求解器何时使用 CP-Solving，何时使用 SAT-Solving？

Question

我成功地使用Google OR Tools解决了一个复杂的匹配问题。 不过我想知道求解器是如何工作的。是否有任何公开论文或书籍可以解释 CP-SAT Solver？因为 cnf 是 Sat-Solver，所以复杂的总和约束真的会转换为 cnf 吗？

我试图找到一些可以深入回答这些问题的公开文章，但我没有找到。

Answer 1

我在这里重新组合了 CP-SAT 的所有资源：

https://github.com/google/or-tools/discussions/4237

目前包含：

• 开发者指南
• github 食谱
• CP-SAT 底漆
• CP-SAT 的工作原理
• CPAIOR 2020大师班
• 研讨会安排