CODEWITHSUNDEEP
pythonz3z3py
Marian Aldenhövel
Marian Aldenhövel

Reputation: 727

Create an or-constraint over a list of Bools

I am playing with Z3 in Python to generate solutions for a dissolution puzzle. I have no prior experience with SAT/SMT solvers or Z3 and even my Python is still at pidgin-level. So please be gentle.

In my approach I have two lists xs and ys of Bools. I know from other constraints that in each of the two lists at most one of the entries is True and all others are False. Either zero or one True entry per list.

I want to add a constraint that compares the two lists on wether they both have a True entry or are both all-False.

So I want something like or(all_the_xs)==or(all_the_ys). I have a feeling this should be pretty native to Z3 but I can't figure out how to state it.

I managed to do it by comparing the count of True-values using z3.Sum([z3.If(x,1,0) for x in xs]) but this does take it out of the realm of simple Booleans. It also feels inelegant and less efficient as possible.

Here is a representative self-contained example of my bodged code using Sum():

import z3

solver = z3.Solver()

xs = [ z3.Bool("x_{i}".format(i=i)) for i in range(0,10) ]
ys = [ z3.Bool("y_{i}".format(i=i)) for i in range(0,10) ]

xsum = z3.Sum([z3.If(x,1,0) for x in xs])
ysum = z3.Sum([z3.If(x,1,0) for x in ys])

solver.add(xsum == ysum)

solver.check()
print(solver.model())

Can you help me restating this in a prettier and more Z3-friendly form? Or assure me it's fine as it is?

Thank you for reading and thinking, Marian

Upvotes: 1

Views: 1430

Answers (1)

alias
alias

Reputation: 30428

You're in luck! z3py comes with Or, which takes a list of booleans:

import z3

solver = z3.Solver()

xs = [ z3.Bool("x_{i}".format(i=i)) for i in range(0,10) ]
ys = [ z3.Bool("y_{i}".format(i=i)) for i in range(0,10) ]

solver.add(z3.Or(xs) == z3.Or(ys))

solver.check()
print(solver.model())

This prints:

[x_0 = False,
 x_1 = False,
 x_2 = False,
 x_3 = False,
 x_4 = False,
 x_5 = False,
 x_6 = False,
 x_7 = False,
 x_8 = False,
 x_9 = False,
 y_0 = False,
 y_1 = False,
 y_2 = False,
 y_3 = False,
 y_4 = False,
 y_5 = False,
 y_6 = False,
 y_7 = False,
 y_8 = False,
 y_9 = False]

Not the most interesting model, but I believe this is precisely what you are looking for!

Upvotes: 3

Related Questions