MAX-SMT guarantees

[m-carrasco]

Hi,

Suppose Optimize is given a MAX-SMT problem and it returns SAT and a model M without timing out. Could a different model M' exist that satisfies all hard constraints and more soft constraints than M?

Best,
Manuel

[NikolajBjorner]

the algorithms are complete. They find models with that are best possible with respect to the cost functions (soft constraints).

[m-carrasco]

Thanks @NikolajBjorner!

This is just to be sure I follow you. In my case, all soft constraints have the same weight (one), so the answer is no. A different model that satisfies more soft constraints cannot exist.

I'm having an issue related to this. I want to be sure first that I understand Z3 correctly.

Apparently, given the same hard and soft constraints sets, the optimizer for two different calls returns two different models that do not satisfy the same number of soft constraints. The two models satisfy two different subsets of soft constraints, which are different in elements and size (by one). I was expecting them to satisfy different subsets but all equal in size. This can be a bug in my code, not necessarily Z3. I'm trying to minimize my example and code.

Again, thanks for your help.

Best,
Manuel.