1

I'm not super savvy on the maths, so please do not destroy me if I've used the wrong terminology here.

What I would like to solve with z3 is something like this:

x + y = z

Assume x, and z are ints.

Where y is an array of constants such as (12,13,14,-13) which may be used, reused, or not used as the solver sees fit.

How would I translate that into z3's functionality? I suspect the answer is generating a constraint for every possible combination of those constants, but I have yet to see an example quite like what I am trying to do.

In other words how would I translate a problem like the "combination of sums" found on many programming interviews such as:

Finding all possible combinations of numbers to reach a given sum

Or

https://leetcode.com/problems/combination-sum/description/

into z3 notation?

To be very precise the piece which is unclear is how to communicate to the solver that it pay pick from an array of choices as many times as it likes.

MrSynAckSter
  • 1,681
  • 1
  • 18
  • 34
  • Care to explain why you are down voting? Other questions similar to this have been accepted on SO before. – MrSynAckSter Oct 21 '17 at 00:43
  • For starters: what is x, what is z; and depending on these: what is ```+```? And is the example integral by pure chance? – sascha Oct 21 '17 at 00:45
  • How is that relevant? I'll change the question but in my experience it would work the same in z3 for whatever data type you wanted to give it. Assume they are ints. My question is about to make z3 choose at will amongst a set of combinations. – MrSynAckSter Oct 21 '17 at 00:47
  • It sounds like I didn't break the rules. You aren't down voting for the right reasons. Also, I changed it. Assume it's ints ok? – MrSynAckSter Oct 21 '17 at 00:49
  • Maybe that might work? I still can't imagine how I'd pass z3 a python array and convert it into a bunch of "or"s like that. And how would you be communicating it can re-use a value as many times as it likes, or not at all? – MrSynAckSter Oct 21 '17 at 01:01
  • You are asking for a Z3-approach and never mentioned python besides the tag. Maybe there are even multiple z3APIs. Details matter! But you got me on that last one: it's missing repeated usage. This means: exhaustive bounded explicit formulation (bad) or checking out z3's theories on what kind of theory supports linear integer arithmetic. Then each of these or's got an nonnegative int-factor in front. – sascha Oct 21 '17 at 01:04
  • And read [this (bitvectors)](https://stackoverflow.com/questions/12326306/need-help-understanding-the-equation) and much more important: [this (nonlin int-arithmetic undecidable and poor support in Z3)](https://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic) (which shows i missed a *non* in my last comment). (Pretty much every SO-answer by this user is interesting; one of z3's devs i think) – sascha Oct 21 '17 at 01:10
  • That might help. FWIW the ultimate use of this is for me to work figure out the order of several "functions" that change the state of x86 registers to figure out how to get to a specific end state. The example I gave was a simplified version using ints, but in real life I would do it with arrays of bit vectors. Since others were using z3 for the same problem, I imagined the normal existing ways of doing it wouldn't be able to deal with the large number of potential combinations. – MrSynAckSter Oct 21 '17 at 01:16
  • Hardware-verification is very much bitvector-stuff correct. Maybe Z3 is used these days; but i remember a lot of SAT-based work (harder to formulate for sure as a more simple logic)! As you recognized: your simplification did nothing useful here (details matters) as mathematical integer-arithmetic is just not hw-based integer-arithmetic (2-complement and co.). Maybe [interesting (Hardware Model Checking Competition 2016)](http://fmv.jku.at/biere/talks/Biere-ARM16-talk.pdf). – sascha Oct 21 '17 at 01:18
  • https://github.com/kokjo/universalrop is one of the examples I was going off of. I sadly cannot comprehend the z3 part of it. It appears he is converting each state transition into a z3 constraint, but how he is telling z3 to pick and choose between them is beyond me. – MrSynAckSter Oct 21 '17 at 01:28

1 Answers1

3

Sure, this is rather easy for any SMT solver. Here's one way to encode it:

from z3 import *

s = Solver()
x = Int("x")
y = Int("y")
z = Int("z")

s.add(Or(y == 12, y == 13, y == 14, y == -13))
s.add(x + y == z)

while s.check() == sat:
    m = s.model ()
    if not m:
        break
    print m
    s.add(Not(And([v() == m[v] for v in m])))

Note that there are infinitely many triplets that satisfy this particular set of constraints, so when you run the above it'll go on printing solutions forever!

To solve the find the subset of numbers that sum up to a number, you can proceed similarly. For each element declare a boolean. Then, write a sum expression that adds all the numbers such that the corresponding boolean is True and assert the constraint that this sum equals the required number. Fun little exercise which is again quite easy to express using Z3. Feel free to ask further questions if you give it a shot and have issues.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Question: How do make the distinction for the solver that each value for Y can be reused? Also, how might you tell the solver to only give you the first n solutions it finds? I suspect that further bounding needs to be added in the constraints themselves. – MrSynAckSter Oct 21 '17 at 23:21
  • 1
    Did you try the above code? It will reuse each value of `y`. For the first `n` solutions, simply keep a count and quit the `while` loop after that many iterations. – alias Oct 22 '17 at 00:43