约束求解技术实战：SAT、SMT与CP的精彩项目解析

我有幸参加了本周早些时候举办的Dagstuhl研讨会，主题是“将CP、SAT和SMT结合在一起”，并了解到了一些之前未曾听闻的非常酷的工作，特别是在约束满足和优化领域。虽然还有许多其他精彩的演讲和讨论，但以下是我记录下来准备尝试的项目。

MiniZinc

“MiniZinc是一种免费开源的约束建模语言。您可以使用MiniZinc以高级、求解器无关的方式对约束满足和优化问题进行建模，同时利用大型预定义约束库。然后您的模型将被编译成FlatZinc，这是一种被广泛求解器理解的求解器输入语言。”

甚至还有几门关于该主题的Coursera课程。

https://www.minizinc.org/ https://www.coursera.org/learn/basic-modeling https://www.coursera.org/learn/advanced-modeling

Unison

“Unison是一个简单、灵活且可能最优的工具，它使用约束编程作为组合优化的现代方法，执行集成的寄存器分配和指令调度。”

https://unison-code.github.io/

近似模型计数

由Mate Soos（cryptominisat的作者）撰写的博客文章，附带代码：

“近似模型计数允许计算命题可满足性问题的解（或‘模型’）数量。鉴于能够找到单个解的命题求解器，这个问题起初看起来很简单：找到一个解，禁止它，请求另一个，再禁止，如此反复直到所有解都被计数。问题在于有时解的数量是2^50，因此这种方式计数太慢。宇宙中大约有2^266个原子，因此使用这种方法计数接近该数量级的解是不可能的。”

https://www.msoos.org/2018/12/how-approximate-model-counting-works/