Find maximum value?

[r4dr3fr4d]

Is it possible in STP to find the maximum value of, eg, a bitvector, a la Z3 optimization/maximization?

[TrevorHansen]

STP doesn't have the functionality to optimise, but it's probably easy for me to implement.

Do you need something like unsigned maximisation of a specified variable in an smt-lib2 format file?

[r4dr3fr4d]

That's what I was looking for - would having both signed and unsigned make sense? I'm trying to think through different use cases...

…

On Fri, May 13, 2022 at 1:23 AM TrevorHansen ***@***.***> wrote: STP doesn't have the functionality to optimise, but it's probably easy for me to implement. Do you need something like unsigned maximisation of a specified variable in an smt-lib2 format file? — Reply to this email directly, view it on GitHub <#425 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACRPRYSLNSXVYNM65SR6SLLVJXRN3ANCNFSM5VZCJIUQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[msoos]

@TrevorHansen wouldn't that require MUS extraction or correction set generation? Those sound pretty complicated, no?

[aytey]

As an FYI: cvc5 implements this with binary search on the optimisation terms

[TrevorHansen]

I was imaging something straightforward, perhaps like CVC implements.

For example, given the 32-bit variable "maximise" in the problem. We'd encode the whole problem to CNF, send it to Cryptominisat(CMS), then ask CMS to assume that the most-significant bit was 1, and so on. Best case 1 call to CMS, worst case there'd be 32 calls to CMS.

[aytey]

Ah, an optimise each term in the order that they're listed in the .smt2 input? So for x + y == 10, if x comes first, you get x=10 and y=0 (I'm purposefully ignoring overflow).

[TrevorHansen]

I was thinking something even easier to implement. E.g. given the input:

(set-logic QF_BV)

(declare-fun maximise () (_ BitVec 32))
(declare-fun v0 () (_ BitVec 32))

(assert (= maximise (bvsmod v0 (_ bv10 32))))
(check-sat)
(get-model)

It'd try to maximise the variable called "maximise" (considering it's unsigned), just by trying to set each bit to 1 in turn.

Is this going to be good enough?

[aytey]

z3 uses (maximize <term>) and (minimize <term>) for this (I think it comes before the check-sat call) -- so calling check-sat does the maximisation/minimisation. afaik, this isn't standard though (e.g., it isn't in SMTLIB or anything like that).

I looked at cvc5 quickly to answer this for myself: I don't think cvc5 supports this via SMTLIB -- looks like it is only via the API.

[aytey]

I guess the idea about iteratively flipping bits (from 0 -> 1) for the maximise case seems reasonable, but we'd need to handle the unsigned case (i.e., you don't want to flip the MSB for signed values).

Bad typo there :)

[msoos]

Binary search on the binary representation! I didn't think of that at all. Of course.

…

On Fri, May 13, 2022, 16:13 Andrew V. Jones ***@***.***> wrote: As an FYI: cvc5 implements this with binary search on the optimisation terms — Reply to this email directly, view it on GitHub <#425 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAKF4OOS2MRUHJ22K5VMOVTVJZPRZANCNFSM5VZCJIUQ> . You are receiving this because you commented.Message ID: ***@***.***>