一些来自Dagstuhl研讨会关于SAT、SMT和CP的酷炫项目
本周我有幸参加了一个名为“将CP、SAT和SMT汇聚一堂”的Dagstuhl研讨会，了解到一些之前未曾听闻的非常酷的工作，尤其是在约束满足和优化领域。虽然还有许多其他精彩的演讲和讨论，但以下是我记录下来的打算尝试的项目。
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是一个简单、灵活且可能最优的工具，它使用约束编程作为组合优化的现代方法，执行集成的寄存器分配和指令调度。”
近似模型计数
Mate Soos（cryptominisat的作者）的博客文章，附有代码： “近似模型计数允许计算命题可满足性问题的解（或‘模型’）数量。这个问题初看似乎很简单，给定一个可以找到单个解的命题求解器：找到一个解，禁止它，请求另一个，禁止它，等等，直到所有解都被计数。问题在于，有时解的数量是2^50，因此以这种方式计数太慢。宇宙中大约有2^266个原子，因此使用这种方法计数接近该数字是不可能的。”