我正在研究研究工具的一个组成部分；我有兴趣检索（对于 QF_LRA）
- 多个（最小或其他）UNSAT 核心和
- 多个 SAT 作业
我已经查看了论坛上有关此主题的早期讨论，例如， 如何在逻辑 QF_LRA 上使用 z3 时获得不同的未饱和内核
他们指的是 z3 Python 教程，例如http://rise4fun.com/Z3Py/tutorial/musmss
现在似乎处于离线状态。我已经尝试了 github 等的其他建议来找到提到的教程，但没有运气。
我正在使用 z3 Java API；但很高兴转向替代品。