一些来自SAT、SMT与CP达格斯特尔研讨会的酷炫项目

本周早些时候，我有幸参加了一个名为“将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/

分享此文章：
点击在Facebook上分享（在新窗口中打开）
Facebook

点击在X上分享（在新窗口中打开）
X
喜欢加载中…

相关文章：

• SAT/SMT暑期学校2011总结（第1天）2011年6月13日，发表于“SMT求解”
• 用于软件安全的SMT求解器（USENIX WOOT’12）2012年7月27日，发表于“漏洞生成”
• SAT/SMT暑期学校2011总结（第2天）2011年6月15日，发表于“SMT求解”

文章导航
上一篇：Fuzzing PHP的unserialize函数
下一篇：利用漏洞模板自动化漏洞生成