-
Notifications
You must be signed in to change notification settings - Fork 128
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Find maximum value? #425
Comments
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? |
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:
***@***.***>
|
@TrevorHansen wouldn't that require MUS extraction or correction set generation? Those sound pretty complicated, no? |
As an FYI: cvc5 implements this with binary search on the optimisation terms |
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. |
Ah, an optimise each term in the order that they're listed in the .smt2 input? So for |
I was thinking something even easier to implement. E.g. given the input:
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? |
z3 uses 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. |
I guess the idea about iteratively flipping bits (from Bad typo there :) |
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:
***@***.***>
|
Is it possible in STP to find the maximum value of, eg, a bitvector, a la Z3 optimization/maximization?
The text was updated successfully, but these errors were encountered: