Z3 выберите числа из массива, чтобы получить сумму - PullRequest
Новая
       89

Z3 выберите числа из массива, чтобы получить сумму

1 голос
/ 09 июля 2020

У меня есть массив чисел в Z3Py: [1.000001, 1.000002, 1.000003, 1.000004, 1.000005, 1.000006, 1.000007, 1.000008, 1.000009, 1.00001, 1.000011, 1.000012, 1.000013, 1.000014, 1.000015, 1.000016, 1.000017, 1.000018, 1.000019, 1.00002, 1.000021, 1.000022, 1.000023, 1.000024, 1.000025, 1.000026, 1.000027, 5.000001, 5.000002, 5.000003, 5.000004, 5.000005, 5.000006, 5.000007, 5.000008, 5.000009, 5.00001] Я хочу выбрать 15 чисел из этого массива, чтобы получить сумму меньше 36.

Как я могу сделать это с помощью Z3Py?

Вот мой код для создания массива: 

possible_students = []
for i in range(1, 28):
    possible_students.append(1 + i / 1000000)
for i in range(1, 11):
    possible_students.append(5 + i / 1000000)

1 Ответ

3 голосов
/ 09 июля 2020

Есть много разных способов решить эту проблему. Вот самая простая кодировка: 

from z3 import *

s = Solver()

nums = [ 1.000001, 1.000002, 1.000003, 1.000004, 1.000005, 1.000006, 1.000007, 1.000008, 1.000009
       , 1.00001 , 1.000011, 1.000012, 1.000013, 1.000014, 1.000015, 1.000016, 1.000017, 1.000018
       , 1.000019, 1.00002 , 1.000021, 1.000022, 1.000023, 1.000024, 1.000025, 1.000026, 1.000027
       , 5.000001, 5.000002, 5.000003, 5.000004, 5.000005, 5.000006, 5.000007, 5.000008, 5.000009
       , 5.00001
       ]

picks = [Bool('p' + str(i)) for i in range(len(nums))]

sum    = Sum([If(p, n, 0) for (p, n) in zip(picks, nums)])
picked = Sum([If(p, 1, 0) for p      in picks])
s.add(picked == 15)
s.add(sum < 36)

r = s.check()
if r == sat:
    m = s.model()
    k = 1
    for i in range(len(nums)):
        if m.eval(picks[i]):
            print("%2d. Picked: %2d: %s" % (k, i, str(nums[i])))
            k = k+1
    print("Sum: " + str(m.eval(sum).as_decimal(10)))
else:
    print("Solver said: " + r)

Когда я запускаю эту программу, я получаю: 

 1. Picked:  4: 1.000005
 2. Picked:  7: 1.000008
 3. Picked:  8: 1.000009
 4. Picked:  9: 1.00001
 5. Picked: 10: 1.000011
 6. Picked: 13: 1.000014
 7. Picked: 15: 1.000016
 8. Picked: 16: 1.000017
 9. Picked: 19: 1.00002
10. Picked: 23: 1.000024
11. Picked: 29: 5.000003
12. Picked: 30: 5.000004
13. Picked: 32: 5.000006
14. Picked: 33: 5.000007
15. Picked: 34: 5.000008
Sum: 35.000162

Надеюсь, это поможет вам начать!

...