How can I put this constraint into Python code?-CodePudding

I am struggling to put the following constraints into python code using Z3 solver, but I am having a hard time. Could anyone please help?

The constraints:

For every X there is at least one Y
For every X there is at most one Y

I tried the below, but it is correct according to the constraint, since the code would only say: Count of x should be lower or equal to count of y.

s = z3.Solver()

x = [1,2,3,4,5,6,7,8]
y = [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]

e_count = len(x)
d_count = len(y)

s.add(d_count =< e_count)

The goal is to assign a y for every x (scheduling problem).

CodePudding user response：

I don't know what your goal is, but you will add boolean value, not a function, to your solver. If I understand correctly, you want to prove that for every x there is at least one y.

Then you can:

y = set(y)
for i in x:
    s.add(i in y)

CodePudding user response：

The easiest way to do this would be to assign a free variable (called picked below) for each x value, assert that it's within the range of ys, and make sure they're distinct. Something like:

from z3 import *

s = Solver()

xs = [1,2,3,4,5,6,7,8]
ys = [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]

# create a picked-value for each x
picked = [Int("picked_%d" % x) for x in xs]

# make sure it's within range
for p in picked:
    s.add(p >= 0)
    s.add(p < len(ys))

# make sure they're distinct
s.add(Distinct(picked))

# get a model:
r = s.check()
if r == sat:
    for (x, p) in zip (xs, picked):
       print(x, " -> ", ys[s.model()[p].as_long()])
else:
    print("Solver said:", r)

This prints:

1  ->  1
2  ->  2
3  ->  3
4  ->  4
5  ->  5
6  ->  6
7  ->  7
8  ->  8

So, unsurprisingly, the solver simply picked for each x the same value in y, as that obviously satisfies the constraints. Once you add further constraints, the model will become more interesting.

(Note that uniqueness of what x value gets matched to is by construction; we pick exactly one value for each x, and the Distinct constraint makes sure there are no repeats.)