Z3 从数组中选择数字以得到总和答案

【问题标题】：Z3 select numbers from array to get sumZ3 从数组中选择数字以得到总和
【发布时间】：2020-07-08 21:21:21
【问题描述】：

我在 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)

【问题讨论】：

欢迎来到 Stack Overflow。你已经尝试过什么来做到这一点？请查看How do I ask a good question 了解我们需要什么。您可以在minimal,reproducible example 中编辑您的问题，详细说明您遇到的确切问题、您尝试解决的问题以及您的相关代码，以便我们提供帮助。
@FluffyKitten -- 谢谢！

标签： z3 solver z3py

【解决方案1】：

可以有许多不同的方法来解决这个问题。这是最直接的编码：

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

希望这能让你开始！

【讨论】：