达格斯图尔研讨会中SAT、SMT与CP的精彩项目

作者有幸参加了本周举办的题为"将CP、SAT和SMT融合"的达格斯图尔研讨会，了解到许多此前未曾接触的创新工作，特别是在约束满足与优化领域。尽管研讨会包含众多精彩演讲与讨论，以下是我特别记录的几个值得深入研究的项目。

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/

近似模型计数

密码迷你SAT作者Mate Soos发布的博客文章及代码： “近似模型计数可用于统计命题可满足性问题的解（或称"模型”）数量。虽然通过命题求解器寻找单个解的方法看似简单（找到一个解后排除，继续寻找直至计数完成），但当解的数量达到2^50量级时，这种计数方式将变得极其缓慢。须知宇宙中原子的总数约为2^266个，接近该量级的计数任务通过传统方法根本无法完成。"

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