How to communicate "signedness" to optimization?

[LeventErkok]

If I have a bit-vector that should be interpreted as a signed quantity, how should I communicate that to the call in maximize/minimize?

If there are operators used around, then z3 seems to be able to "infer" the signedness (though I think this may not be enough either.) But in the extreme case when there is nothing but the type, I'm not sure how to communicate this properly.

As a concrete input, consider this:

(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun s0 () (_ BitVec 8))
(maximize s0)
(check-sat)
(get-objectives)
(get-value (s0))

This rightfully produces:

sat
(objectives
 (s0 255)
)
((s0 #xff))

But what should I do to tell the solver that s0 is actually to be interpreted as a signed quantity, and hence the maximum value it can actually take is 127?

It almost looks like we need umaximize/smaximize/uminimize/sminimize to communicate the intent, following the similar operators in the bit-vector theory. Or, is there a trick I can use to make sure this is communicated properly?

Thanks!

[andersk]

smaximize on an n-bit signed bitvector x would be equivalent to (u)maximize on the n-bit unsigned bitvector x + 2^{n − 1}.

[NikolajBjorner]

or maybe x + 2^{n-1} + most-significant-bit(x), but the overall point is that the objective can be transformed. Perhaps not user-friendly.

Another point to clarify is that Z3 has no special heuristics when optimizing bit-vectors. There are two approaches/papers that tune for this case (one with Mathias Soeken and one with Alex Nadel) but Z3 does not take this into account. If this is a common use case for you, then a strategy that optimizes one bit at a time and otherwise uses partial information from the process will scale better.

[andersk]

@NikolajBjorner I don’t know where you’re getting “+ most-significant-bit(x)”. The transformation as I wrote it is the unique order-preserving map from the signed range [−2^{n − 1}, 2^{n − 1}) to the unsigned range [0, 2ⁿ).

[LeventErkok]

Thanks @NikolajBjorner

I think @andersk is right that all we need to add is 2^{n-1}. Can you confirm?

But even then, I think it would be in the "spirit" of the BV operators to add signed/unsigned variants of maximize/minimize; and Z3 can lead the way here as other solvers usually follow suit and this is likely to be a gotcha for many users and all the tools built on top. What are your thoughts on supporting this directly in Z3?

[NikolajBjorner]

Are you also going to ask for a signed bv2int? e.g., there could be several other places where being consequent about supporting signed semantics would be called for.

[LeventErkok]

I wasn't going to, but now that you mention it. :-)

But seriously; this is a "nice to have" as the workaround is rather cumbersome. But it's not the end of the world.

I'll close this ticket, though if you feel generous enough and decide to add support, feel free to re-open!

[NikolajBjorner]

I see it as a tradeoff between feature creep and making common cases easy. Since we don't even optimize optimally for bit-vectors the best I could do is to support this part before the interface features.

[PatrickTrentin88]

@NikolajBjorner @LeventErkok I was wondering if the optimization language was extended to support this feature as suggested in the opening thread, or not. It would be helpful to know before OptiMathSAT and z3 end up having yet another input language mismatch :-)

The options, as far as I can see them are:

 uminimize, umaximize, sminimize, smaximize

or

 ([minimize|maximize] <term> [:signed true|false])

with :signed false as default.