CODEWITHSUNDEEP
pythonz3solversmtz3py
DonVitoMarco
DonVitoMarco

Reputation: 21

Find the minimum number of elements in the set using z3py

Exercise: Find the minimum number of elements in the set Z that add up to 4285. Where Z = { w(i): w(n) - n^2 - n + 1, i = 1,2,...,30 }

I created a solution: 

def f(t):
    return t ** 2 - t + 1


opt = z3.Optimize()

x = IntVector('x', 30)
x_val = [And(x[i] >= 0, x[i] <= 1) for i in range(30)]
opt.add(x_val)

m = [x[i] * f(i + 1) for i in range(30)]
m_sum = z3.Sum(m)

opt.add(m_sum == 4285)
opt.minimize(z3.Sum(x))

if z3.sat == opt.check():
    model = opt.model()
    print(model)

but it works too slowly. Works only for small numbers. How can I improve it?

Upvotes: 2

Views: 567

Answers (2)

Axel Kemper
Axel Kemper

Reputation: 11322

Not an answer but a confirmation of the 7-bit solution proposed by alias.

I tried the following MiniZinc model:

int: n = 30;
set of int: N = 1..n;

function int: f(int: t) =
  t*t - t + 1;

array[N] of var bool: x;

constraint ( 4285 == sum([x[i] * f(i) | i in N]) );

var int: bitCount = sum([ x[i] | i in N]);

solve minimize bitCount;

output ["#\(bitCount): "] ++
       ["\(if x[i] then 1 else 0 endif)" | i in N];

Result:

#7: 000000000000000010001001011011

Upvotes: 1

alias
alias

Reputation: 30525

It's almost always a bad idea to represent booleans by integers in z3. So, instead of using an integer vector where you say items are between 0-1, simply use a boolean vector and the If construct. Something like this:

from z3 import *

def f(t):
    return t ** 2 - t + 1

opt = z3.Optimize()

x = BoolVector('x', 30)

m = [If(x[i], f(i + 1), 0) for i in range(30)]
m_sum = z3.Sum(m)

opt.add(m_sum == 4285)

opt.minimize(z3.Sum([If(x[i], 1, 0) for i in range(30)]))

if z3.sat == opt.check():
    model = opt.model()
    print(model)

When I run this, it goes really quickly and finds the solution:

[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,
 x__10 = False,
 x__11 = False,
 x__12 = False,
 x__13 = True,
 x__14 = False,
 x__15 = False,
 x__16 = False,
 x__17 = True,
 x__18 = False,
 x__19 = False,
 x__20 = False,
 x__21 = False,
 x__22 = False,
 x__23 = False,
 x__24 = False,
 x__25 = True,
 x__26 = True,
 x__27 = True,
 x__28 = True,
 x__29 = True]

I didn't check if this is the right solution, but at least it should get you started!

Upvotes: 3

Related Questions