CODEWITHSUNDEEP
z3
Dingbao Xie
Dingbao Xie

Reputation: 736

possible to extract an unsat core when using 'nlsat' solver

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.

Upvotes: 2

Views: 128

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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.

Upvotes: 3

Related Questions