约束求解：达戈斯图尔研讨会中的酷炫项目

本周我有幸参加了题为"将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/

近似模型计数

这是cryptominisat作者Mate Soos撰写的博客文章（附代码）： “近似模型计数可以统计命题可满足性问题的解（或称’模型’）数量。这个问题初看似乎很简单：找到一个解后将其排除，继续寻找下一个，如此重复直到统计完所有解。但问题在于有时解的数量会达到2^50量级，这种统计方式将变得极其缓慢。宇宙中原子数量约为2^266个，因此使用这种方法统计接近该量级的解数是不可能的。”

技术详解：https://www.msoos.org/2018/12/how-approximate-model-counting-works/