Example of MAXSMT?

[varunpatro]

Hello!

I saw here that Z3 supports having hard and soft constraints using assert-soft. However, I'm wondering if you know how I can use the python API to do that?

Cheers,
Varun

[0vercl0k]

Hey there man! Interesting, I didn't even know it was supporting soft/hard constraints. It's been awhile I didn't look at z3py and so I'm a bit outdated on the potential new features. So to answer your question, no I've no clue how to do that :-D. I'll try to look into it in the next weeks. If you find a way before I get to look at it, feel free to drop an example here :). Cheers 2018-03-13 7:52 GMT-07:00 Varun Patro <notifications@github.com>:

…

Hello! I saw here <https://rise4fun.com/Z3/tutorialcontent/optimization> that Z3 supports having hard and soft constraints using assert-soft. However, I'm wondering if you know how I can use the python API to do that? Cheers, Varun — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#4>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABaHRSN9T2UaLqLN73WgPfZdAtoi58ERks5td905gaJpZM4So1GG> .

[varunpatro]

Thanks for the work on this repo, by the way :-) it definitely made it easier to get started. Z3 has been for the most part, quite useful to me so far.

I've finally figured out how to use the hard/soft constraints. I'll try to write them up proper and send a PR when I get some time. Meanwhile, I just wanted to share a simple example, in case it helps other people out there:

from z3 import *
x, y = Ints('x y')
z = x + y

opt = Optimize()

# hard constraints
# e.g. `add(<constraint>)`
opt.add(z == 0)
if opt.check() == sat:
    print opt.model() # should print [y = 0, x = 0]
else:
    print 'unsat'

# soft constraints 
# e.g. `add_soft(<constraint>, <constraint_weight>)`
opt.add_soft(x > 5, 10)
opt.add_soft(y > 5, 15)

if opt.check() == sat:
    print opt.model() # should print [y = 6, x = -6] because y > 5 has a larger weight than x > 5
else:
    print 'unsat'

[0vercl0k]

Super cool - thanks man! Looking forward to seeing your PR then :). Cheers 2018-03-18 8:26 GMT-07:00 Varun Patro <notifications@github.com>:

…

Thanks for the work on this repo, by the way :-) it definitely made it easier to get started. Z3 has been for the most part, quite useful to me so far. I've finally figured out how to use the hard/soft constraints. I'll try to write them up proper and send a PR when I get some time. Meanwhile, I just wanted to share a simple example, in case it helps other people out there: from z3 import * x, y = Ints('x y') z = x + y opt = Optimize() # hard constraints# e.g. `add(<constraint>)` opt.add(z == 0)if opt.check() == sat: print opt.model() # should print [y = 0, x = 0]else: print 'unsat' # soft constraints # e.g. `add_soft(<constraint>, <constraint_weight>)` opt.add_soft(x > 5, 10) opt.add_soft(y > 5, 15) if opt.check() == sat: print opt.model() # should print [y = 6, x = -6] because y > 5 has a larger weight than x > 5else: print 'unsat' — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#4 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABaHRdJvOwugjJWJ5OdDOs45bJNAk48Pks5tfnyVgaJpZM4So1GG> .