使用“nlsat”求解器时可以提取未饱和核心

Question

在上一个问题solve nonlinear constraints中，我问z3在使用nlsat求解器处理非线性实数算术的多项式约束时，是否可以给出一个合理且完整的结果。正如 Taylor 回答的那样，nksat 求解器是完整且可靠的。

Z3 在解决 LRA 上的约束时支持 unsat core 提取。我想知道是否 使用 nlsat 求解器时可以提取 unsat 核心吗？如果z3不支持， 我可以在 z3 之上实现它吗？另一个问题是它可以处理多大的问题。

Answer 1

非线性约束的求解器不支持核心提取，因此您将无法直接检索核心。您可以在 Z3 之上为（最小）核心实现二等分搜索（快速解释）。这将需要多次调用，因此它是否要取决于您的应用程序 实用。