2

In the previous question solve nonlinear constraints, I asked whether z3 could give a sound and complete result when using nlsat solver to handle polynomial constraints on nonlinear real arithmetic. As Taylor answered, the nksat solver is complete and sound.

Z3 supports unsat core extraction when solving constraints on LRA. I want to know that whether it possible to extract an unsat core when using the nlsat solver? If z3 does not support, can I implement it on top of z3? A further question is how large problem it can handle.

Community
  • 1
  • 1
Dingbao Xie
  • 716
  • 9
  • 21

1 Answers1

3

The solver for non-linear constraints does not support core extraction so you will not be able to retrieve a core directly. You can implement a bisection search (quick-explain) on top of Z3 for a (minimal) core. It will require several calls so it depends on your application if it is going to be practical.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15