在阅读了前面的问题Getting a "good" unsat core and getting new unsat core之后，我知道目前用 z3 不可能得到多个不同的 unsat core。你有什么建议可以让 unsat core 变小吗？我正在使用 z3 c++ api 来检查线性实数算术约束的可满足性。我发现当按照Getting a "good" unsat corep.set(":auto-config",false)中的建议添加这行代码时，unsat core的大小会变小。
另一个问题是关于 z3 的基于单纯形的算法。在使用 z3 之前，我已经使用 CPLEX 解决了我的应用程序。CPLEX 支持提取 IIS（不可约不可行集），类似于 z3 中的 unsat 核心。我们可以在 CPLEX 中将求解算法设置为“auto”、“primal”、“dual”。我发现切换 IIS CPLEX 给出的求解算法时可能会有所不同。当逻辑设置为 QF_LRA 时，z3 是否支持设置不同的求解算法？