CODEWITHSUNDEEP
pythonz3smt
MrSynAckSter
MrSynAckSter

Reputation: 1770

z3: How to solve for combinations for a set of constants?

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.

Upvotes: 1

Views: 1722

Answers (1)

alias
alias

Reputation: 30460

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.

Upvotes: 4

Related Questions