组合z3中给定项集的元素

下面的z3代码从 {x1..x6} 为了最大化总重量,同时满足总长度小于10。

(declare-datatypes () ((Item (mk-item (size Int) (weight Int)))))

(define-fun ee () Item (mk-item 0 0)); empty item
(define-fun i1 () Item (mk-item 4 2))
(define-fun i2 () Item (mk-item 4 2))
(define-fun i3 () Item (mk-item 1 4))
(define-fun i4 () Item (mk-item 5 5))
(define-fun i5 () Item (mk-item 3 2))
(define-fun i6 () Item (mk-item 1 9))

(define-fun x_props ((x Bool) (i Item)) Item (ite x i ee))

; each x defines whether an item is selected or not
(declare-const x1 Bool)
(declare-const x2 Bool)
(declare-const x3 Bool)
(declare-const x4 Bool)
(declare-const x5 Bool)
(declare-const x6 Bool)

(define-fun total_size () Int
  (+
    (size (x_props x1 i1))
    (size (x_props x2 i2))
    (size (x_props x3 i3))
    (size (x_props x4 i4))
    (size (x_props x5 i5))
    (size (x_props x6 i6))
  ))

(define-fun total_weight () Int
  (+
    (weight (x_props x1 i1))
    (weight (x_props x2 i2))
    (weight (x_props x3 i3))
    (weight (x_props x4 i4))
    (weight (x_props x5 i5))
    (weight (x_props x6 i6))
  ))

(assert (< total_size 10))
(maximize total_weight)

(check-sat)
(get-model)

然而,我可以想象,随着项目属性的数量激增,以及项目的数量激增,这种缩放非常糟糕。

会有一种不同的、更简洁的方法吗?特别是,你能想出一种方法来分解 total_size 和 total_weight 功能,因为有很多重复?