0

I know that you can add soft-constraint in z3py and then ask z3 to find a model that satisfies the maximum number of soft-constraints possible by running:

s = Optimize()
s.add_soft(...)
...
s.add_soft(...)
s.check()

My questions is what can you do if you want z3 to return any model that satisfies at least k soft-constraints. My hope is that if z3 managed to satisfy k constraints it will stop the search and return the current model.

alias
  • 28,120
  • 2
  • 23
  • 40
Andrei Draghici
  • 1

1 Answers1

0

Yes. These are called k-out-of-N constraints, also known as pseudo-boolean constraints. See K-out-of-N constraint in Z3Py for details.

alias
  • 28,120
  • 2
  • 23
  • 40