达格斯图尔研讨会中一些很酷的项目

我很幸运地参加了本周早些时候举行的名为"将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/