0

根据我的经验，在较大型号的情况下，我发现与饱和情况相比，Z3 需要更长的时间才能给出不饱和结果。甚至有时Z3会无限运行而没有给出任何答案。下面我举一个这样的例子。[虽然我使用 .NET API 进行形式化，但我在这里写的是等效的 SMT-LIB 2 代码。]

(declare-fun VCapacity (Int) Int)
(declare-fun VChargeInit (Int) Int)
(declare-fun VChargeEnd (Int) Int)
(declare-fun VStartAt (Int) Int)
(declare-fun VEndAt (Int) Int)
(declare-fun VCRate (Int) Int)
(declare-fun VChargeAt (Int Int) Int)
(declare-fun VFunctionAt (Int Int) Int)
(declare-fun VCCharge (Int Int) Int)
(declare-fun VCDischarge (Int Int) Int)
(declare-fun VCFReg (Int Int) Int)
(declare-fun TotalCChargeAt (Int) Int)
(declare-fun TotalCDischargeAt (Int) Int)
(declare-fun TotalCFRegAt (Int) Int)

(declare-const Total Int)


(assert (and (= (VStartAt 1) 1)
     (= (VEndAt 1) 4)
     (= (VCapacity 1) 30)
     (= (VChargeEnd 1) 20)
     (= (VCRate 1) 10)
     (= (VChargeInit 1) 10)
     (= (VChargeAt 1 0) 10)))
(assert (and (= (VChargeAt 1 5) 0)
     (= (VChargeAt 1 6) 0)
     (= (VChargeAt 1 7) 0)
     (= (VChargeAt 1 8) 0)))
(assert (and (= (VStartAt 2) 2)
     (= (VEndAt 2) 7)
     (= (VCapacity 2) 40)
     (= (VChargeEnd 2) 30)
     (= (VCRate 2) 10)
     (= (VChargeInit 2) 20)
     (= (VChargeAt 2 1) 20)))
(assert (and (= (VChargeAt 2 0) 0) (= (VChargeAt 2 8) 0)))
(assert (and (= (VStartAt 3) 4)
     (= (VEndAt 3) 6)
     (= (VCapacity 3) 20)
     (= (VChargeEnd 3) 20)
     (= (VCRate 3) 10)
     (= (VChargeInit 3) 10)
     (= (VChargeAt 3 3) 10)))
(assert (and (= (VChargeAt 3 0) 0)
     (= (VChargeAt 3 1) 0)
     (= (VChargeAt 3 2) 0)
     (= (VChargeAt 3 7) 0)
     (= (VChargeAt 3 8) 0)))
(assert (and (= (VStartAt 4) 5)
     (= (VEndAt 4) 8)
     (= (VCapacity 4) 30)
     (= (VChargeEnd 4) 20)
     (= (VCRate 4) 10)
     (= (VChargeInit 4) 0)
     (= (VChargeAt 4 4) 0)))
(assert (and (= (VChargeAt 4 0) 0)
     (= (VChargeAt 4 1) 0)
     (= (VChargeAt 4 2) 0)
     (= (VChargeAt 4 3) 0)))

(assert (forall ((V Int)) (implies (and (>= V 1) (<= V 4)) (>= (VCapacity V) 10))))

(assert (forall ((V Int) (S Int))
  (implies (and (>= V 1) (<= V 4) (>= S 1) (<= S 8))
           (and (>= (VFunctionAt V S) 0) (<= (VFunctionAt V S) 3)))))

(assert (forall ((V Int) (S Int))
  (implies (and (and (>= V 1) (<= V 4) (>= S 1) (<= S 8))
                (or (and (>= S 1) (< S (VStartAt V)))
                    (and (> S (VEndAt V)) (<= S 8))))
           (= (VFunctionAt V S) 0))))

(assert (forall ((V Int) (S Int))
  (implies (and (>= V 1) (<= V 4) (>= S (VStartAt V)) (<= S (VEndAt V)))
           (and (implies (= (VFunctionAt V S) 0)
                         (= (VChargeAt V S) (VChargeAt V (- S 1))))
                (implies (= (VFunctionAt V S) 1)
                         (and (< (VChargeAt V (- S 1)) (VCapacity V))
                              (if (< (VCapacity V)
                                     (+ (VChargeAt V (- S 1)) (VCRate V)))
                                  (and (= (VChargeAt V S) (VCapacity V))
                                       (= (VCCharge V S)
                                          (- (VCapacity V)
                                             (VChargeAt V (- S 1)))))
                                  (and (= (VChargeAt V S)
                                          (+ (VChargeAt V (- S 1)) (VCRate V)))
                                       (= (VCCharge V S) (VCRate V))))))
                (implies (= (VFunctionAt V S) 2)
                         (and (> (VChargeAt V (- S 1)) 0)
                              (if (< (- (VChargeAt V (- S 1)) (VCRate V)) 0)
                                  (and (= (VChargeAt V S) 0)
                                       (= (VCDischarge V S)
                                          (VChargeAt V (- S 1))))
                                  (and (= (VChargeAt V S)
                                          (- (VChargeAt V (- S 1)) (VCRate V)))
                                       (= (VCDischarge V S) (VCRate V))))))
                (implies (= (VFunctionAt V S) 3)
                         (and (= (VChargeAt V S) (VChargeAt V (- S 1)))
                              (= (VCFReg V S) (VChargeAt V (- S 1)))))))))

(assert (forall ((V Int))
  (implies (and (>= V 1) (<= V 4)) (>= (VChargeAt V (VEndAt V)) (VChargeEnd V)))))

(assert (forall ((V Int) (S Int))
  (implies (and (>= V 1) (<= V 4) (>= S 1) (<= S 8))
           (and (implies (= (VFunctionAt V S) 0)
                         (and (= (VCCharge V S) 0)
                              (= (VCDischarge V S) 0)
                              (= (VCFReg V S) 0)))
                (implies (= (VFunctionAt V S) 1)
                         (and (> (VCCharge V S) 0)
                              (= (VCDischarge V S) 0)
                              (= (VCFReg V S) 0)))
                (implies (= (VFunctionAt V S) 2)
                         (and (= (VCCharge V S) 0)
                              (> (VCDischarge V S) 0)
                              (= (VCFReg V S) 0)))
                (implies (= (VFunctionAt V S) 3)
                         (and (= (VCCharge V S) 0)
                              (= (VCDischarge V S) 0)
                              (> (VCFReg V S) 0)))))))

(assert (= (TotalCChargeAt 1)
   (+ (VCCharge 1 1) (VCCharge 2 1) (VCCharge 3 1) (VCCharge 4 1))))
(assert (= (TotalCDischargeAt 1)
   (+ (VCDischarge 1 1) (VCDischarge 2 1) (VCDischarge 3 1) (VCDischarge 4 1))))
(assert (= (TotalCFRegAt 1) (+ (VCFReg 1 1) (VCFReg 2 1) (VCFReg 3 1) (VCFReg 4 1))))
(assert (= (TotalCChargeAt 2)
   (+ (VCCharge 1 2) (VCCharge 2 2) (VCCharge 3 2) (VCCharge 4 2))))
(assert (= (TotalCDischargeAt 2)
   (+ (VCDischarge 1 2) (VCDischarge 2 2) (VCDischarge 3 2) (VCDischarge 4 2))))
(assert (= (TotalCFRegAt 2) (+ (VCFReg 1 2) (VCFReg 2 2) (VCFReg 3 2) (VCFReg 4 2))))
(assert (= (TotalCChargeAt 3)
   (+ (VCCharge 1 3) (VCCharge 2 3) (VCCharge 3 3) (VCCharge 4 3))))
(assert (= (TotalCDischargeAt 3)
   (+ (VCDischarge 1 3) (VCDischarge 2 3) (VCDischarge 3 3) (VCDischarge 4 3))))
(assert (= (TotalCFRegAt 3) (+ (VCFReg 1 3) (VCFReg 2 3) (VCFReg 3 3) (VCFReg 4 3))))
(assert (= (TotalCChargeAt 4)
   (+ (VCCharge 1 4) (VCCharge 2 4) (VCCharge 3 4) (VCCharge 4 4))))
(assert (= (TotalCDischargeAt 4)
   (+ (VCDischarge 1 4) (VCDischarge 2 4) (VCDischarge 3 4) (VCDischarge 4 4))))
(assert (= (TotalCFRegAt 4) (+ (VCFReg 1 4) (VCFReg 2 4) (VCFReg 3 4) (VCFReg 4 4))))
(assert (= (TotalCChargeAt 5)
   (+ (VCCharge 1 5) (VCCharge 2 5) (VCCharge 3 5) (VCCharge 4 5))))
(assert (= (TotalCDischargeAt 5)
   (+ (VCDischarge 1 5) (VCDischarge 2 5) (VCDischarge 3 5) (VCDischarge 4 5))))
(assert (= (TotalCFRegAt 5) (+ (VCFReg 1 5) (VCFReg 2 5) (VCFReg 3 5) (VCFReg 4 5))))
(assert (= (TotalCChargeAt 6)
   (+ (VCCharge 1 6) (VCCharge 2 6) (VCCharge 3 6) (VCCharge 4 6))))
(assert (= (TotalCDischargeAt 6)
   (+ (VCDischarge 1 6) (VCDischarge 2 6) (VCDischarge 3 6) (VCDischarge 4 6))))
(assert (= (TotalCFRegAt 6) (+ (VCFReg 1 6) (VCFReg 2 6) (VCFReg 3 6) (VCFReg 4 6))))
(assert (= (TotalCChargeAt 7)
   (+ (VCCharge 1 7) (VCCharge 2 7) (VCCharge 3 7) (VCCharge 4 7))))
(assert (= (TotalCDischargeAt 7)
   (+ (VCDischarge 1 7) (VCDischarge 2 7) (VCDischarge 3 7) (VCDischarge 4 7))))
(assert (= (TotalCFRegAt 7) (+ (VCFReg 1 7) (VCFReg 2 7) (VCFReg 3 7) (VCFReg 4 7))))
(assert (= (TotalCChargeAt 8)
   (+ (VCCharge 1 8) (VCCharge 2 8) (VCCharge 3 8) (VCCharge 4 8))))
(assert (= (TotalCDischargeAt 8)
   (+ (VCDischarge 1 8) (VCDischarge 2 8) (VCDischarge 3 8) (VCDischarge 4 8))))
(assert (= (TotalCFRegAt 8) (+ (VCFReg 1 8) (VCFReg 2 8) (VCFReg 3 8) (VCFReg 4 8))))
(assert (and (or (= (TotalCFRegAt 1) 0) (>= (TotalCFRegAt 1) 20))
     (or (= (TotalCDischargeAt 1) 0)
         (and (<= (TotalCDischargeAt 1) 30) (>= (TotalCDischargeAt 1) 10)))
     (or (= (TotalCChargeAt 1) 0) (<= (TotalCChargeAt 1) 60))))
(assert (and (or (= (TotalCFRegAt 2) 0) (>= (TotalCFRegAt 2) 20))
     (or (= (TotalCDischargeAt 2) 0)
         (and (<= (TotalCDischargeAt 2) 30) (>= (TotalCDischargeAt 2) 10)))
     (or (= (TotalCChargeAt 2) 0) (<= (TotalCChargeAt 2) 60))))
(assert (and (or (= (TotalCFRegAt 3) 0) (>= (TotalCFRegAt 3) 20))
     (or (= (TotalCDischargeAt 3) 0)
         (and (<= (TotalCDischargeAt 3) 40) (>= (TotalCDischargeAt 3) 10)))
     (or (= (TotalCChargeAt 3) 0) (<= (TotalCChargeAt 3) 50))))
(assert (and (or (= (TotalCFRegAt 4) 0) (>= (TotalCFRegAt 4) 35))
     (or (= (TotalCDischargeAt 4) 0)
         (and (<= (TotalCDischargeAt 4) 30) (>= (TotalCDischargeAt 4) 10)))
     (or (= (TotalCChargeAt 4) 0) (<= (TotalCChargeAt 4) 30))))
(assert (and (or (= (TotalCFRegAt 5) 0) (>= (TotalCFRegAt 5) 25))
     (or (= (TotalCDischargeAt 5) 0)
         (and (<= (TotalCDischargeAt 5) 40) (>= (TotalCDischargeAt 5) 20)))
     (or (= (TotalCChargeAt 5) 0) (<= (TotalCChargeAt 5) 40))))
(assert (and (or (= (TotalCFRegAt 6) 0) (>= (TotalCFRegAt 6) 35))
     (or (= (TotalCDischargeAt 6) 0)
         (and (<= (TotalCDischargeAt 6) 40) (>= (TotalCDischargeAt 6) 10)))
     (or (= (TotalCChargeAt 6) 0) (<= (TotalCChargeAt 6) 40))))
(assert (and (or (= (TotalCFRegAt 7) 0) (>= (TotalCFRegAt 7) 20))
     (or (= (TotalCDischargeAt 7) 0)
         (and (<= (TotalCDischargeAt 7) 30) (>= (TotalCDischargeAt 7) 10)))
     (or (= (TotalCChargeAt 7) 0) (<= (TotalCChargeAt 7) 50))))
(assert (and (or (= (TotalCFRegAt 8) 0) (>= (TotalCFRegAt 8) 20))
     (or (= (TotalCDischargeAt 8) 0)
         (and (<= (TotalCDischargeAt 8) 30) (>= (TotalCDischargeAt 8) 10)))
     (or (= (TotalCChargeAt 8) 0) (<= (TotalCChargeAt 8) 60))))

(assert (= (+ (- (+ (* (TotalCDischargeAt 1) 1) (* (TotalCFRegAt 1) 1))
          (* (TotalCChargeAt 1) 1))
       (- (+ (* (TotalCDischargeAt 2) 1) (* (TotalCFRegAt 2) 1))
          (* (TotalCChargeAt 2) 1))
       (- (+ (* (TotalCDischargeAt 3) 1) (* (TotalCFRegAt 3) 1))
          (* (TotalCChargeAt 3) 1))
       (- (+ (* (TotalCDischargeAt 4) 2) (* (TotalCFRegAt 4) 2))
          (* (TotalCChargeAt 4) 2))
       (- (+ (* (TotalCDischargeAt 5) 2) (* (TotalCFRegAt 5) 1))
          (* (TotalCChargeAt 5) 2))
       (- (+ (* (TotalCDischargeAt 6) 2) (* (TotalCFRegAt 6) 2))
          (* (TotalCChargeAt 6) 2))
       (- (+ (* (TotalCDischargeAt 7) 1) (* (TotalCFRegAt 7) 1))
          (* (TotalCChargeAt 7) 1))
       (- (+ (* (TotalCDischargeAt 8) 1) (* (TotalCFRegAt 8) 1))
          (* (TotalCChargeAt 8) 1)))
    Total))

(assert (>= Total 350))

(check-sat)
(get-model)

在我的形式化中，我主要使用未解释的函数。在这个例子中，我只显示了 4 辆车 (1<=V<= 4) 和 4 个时隙 (1<=S<=4)。在这里，在 unsat 结果的情况下，求解器花费的时间几乎是 sat 结果情况的 40 倍。当我们增加大小，例如6辆车和8个槽位（如下图），并将最小收益（即Total）设置为更大的值（例如，600），它会持续运行很长时间而不给出任何答案（期待一个不满意的结果）。但是，在饱和情况下（最低收益较低），Z3 需要几秒钟。由于车辆/插槽数量的小幅增加，sat 和 unsat 情况下的性能显着降低，尽管 unsat 情况下的性能很糟糕。

(set-option :relevancy 0)

(declare-fun VCapacity (Int) Int)
(declare-fun VChargeInit (Int) Int)
(declare-fun VChargeEnd (Int) Int)
(declare-fun VStartAt (Int) Int)
(declare-fun VEndAt (Int) Int)
(declare-fun VCRate (Int) Int)
(declare-fun VChargeAt (Int Int) Int)
(declare-fun VFunctionAt (Int Int) Int)
(declare-fun VCCharge (Int Int) Int)
(declare-fun VCDischarge (Int Int) Int)
(declare-fun VCFReg (Int Int) Int)
(declare-fun TotalCChargeAt (Int) Int)
(declare-fun TotalCDischargeAt (Int) Int)
(declare-fun TotalCFRegAt (Int) Int)

(declare-const Total Int)

; Input to the model
(assert (and (= (VStartAt 1) 1)
     (= (VEndAt 1) 4)
     (= (VCapacity 1) 30)
     (= (VChargeEnd 1) 20)
     (= (VCRate 1) 10)
     (= (VChargeInit 1) 10)
     (= (VChargeAt 1 0) 10)))
(assert (and (= (VChargeAt 1 5) 0)
     (= (VChargeAt 1 6) 0)
     (= (VChargeAt 1 7) 0)
     (= (VChargeAt 1 8) 0)))
(assert (and (= (VStartAt 2) 2)
     (= (VEndAt 2) 7)
     (= (VCapacity 2) 40)
     (= (VChargeEnd 2) 30)
     (= (VCRate 2) 10)
     (= (VChargeInit 2) 20)
     (= (VChargeAt 2 1) 20)))
(assert (and (= (VChargeAt 2 0) 0) (= (VChargeAt 2 8) 0)))
(assert (and (= (VStartAt 3) 4)
     (= (VEndAt 3) 6)
     (= (VCapacity 3) 20)
     (= (VChargeEnd 3) 20)
     (= (VCRate 3) 10)
     (= (VChargeInit 3) 10)
     (= (VChargeAt 3 3) 10)))
(assert (and (= (VChargeAt 3 0) 0)
     (= (VChargeAt 3 1) 0)
     (= (VChargeAt 3 2) 0)
     (= (VChargeAt 3 7) 0)
     (= (VChargeAt 3 8) 0)))
(assert (and (= (VStartAt 4) 5)
     (= (VEndAt 4) 8)
     (= (VCapacity 4) 30)
     (= (VChargeEnd 4) 20)
     (= (VCRate 4) 10)
     (= (VChargeInit 4) 0)
     (= (VChargeAt 4 4) 0)))
(assert (and (= (VChargeAt 4 0) 0)
     (= (VChargeAt 4 1) 0)
     (= (VChargeAt 4 2) 0)
     (= (VChargeAt 4 3) 0)))
(assert (and (= (VStartAt 5) 2)
     (= (VEndAt 5) 6)
     (= (VCapacity 5) 20)
     (= (VChargeEnd 5) 20)
     (= (VCRate 5) 10)
     (= (VChargeInit 5) 10)
     (= (VChargeAt 5 1) 10)))
(assert (and (= (VChargeAt 5 0) 0) (= (VChargeAt 5 7) 0) (= (VChargeAt 5 8) 0)))
(assert (and (= (VStartAt 6) 4)
     (= (VEndAt 6) 7)
     (= (VCapacity 6) 30)
     (= (VChargeEnd 6) 20)
     (= (VCRate 6) 10)
     (= (VChargeInit 6) 0)
     (= (VChargeAt 6 3) 0)))
(assert (and (= (VChargeAt 6 0) 0)
     (= (VChargeAt 6 1) 0)
     (= (VChargeAt 6 2) 0)
     (= (VChargeAt 6 8) 0)))

; A vehicle battery's capacity should be greater than some threshold value     
(assert (forall ((V Int)) (implies (and (>= V 1) (<= V 6)) (>= (VCapacity V) 10))))

; A vehicle has 4 options (0 to 3) as its function
(assert (forall ((V Int) (S Int))
  (implies (and (>= V 1) (<= V 6) (>= S 1) (<= S 8))
           (and (>= (VFunctionAt V S) 0) (<= (VFunctionAt V S) 3)))))

; For slots before and after the available period, the function is 0 (idle)           
(assert (forall ((V Int) (S Int))
  (implies (and (and (>= V 1) (<= V 6) (>= S 1) (<= S 8))
                (or (and (>= S 1) (< S (VStartAt V)))
                    (and (> S (VEndAt V)) (<= S 8))))
           (= (VFunctionAt V S) 0))))

; Update the vehicle's stored energy/charge           
(assert (forall ((V Int) (S Int))
  (implies (and (>= V 1) (<= V 6) (>= S (VStartAt V)) (<= S (VEndAt V)))
           (and (implies (= (VFunctionAt V S) 0)
                         (= (VChargeAt V S) (VChargeAt V (- S 1))))
                (implies (= (VFunctionAt V S) 1)
                         (and (< (VChargeAt V (- S 1)) (VCapacity V))
                              (if (< (VCapacity V)
                                     (+ (VChargeAt V (- S 1)) (VCRate V)))
                                  (and (= (VChargeAt V S) (VCapacity V))
                                       (= (VCCharge V S)
                                          (- (VCapacity V)
                                             (VChargeAt V (- S 1)))))
                                  (and (= (VChargeAt V S)
                                          (+ (VChargeAt V (- S 1)) (VCRate V)))
                                       (= (VCCharge V S) (VCRate V))))))
                (implies (= (VFunctionAt V S) 2)
                         (and (> (VChargeAt V (- S 1)) 0)
                              (if (< (- (VChargeAt V (- S 1)) (VCRate V)) 0)
                                  (and (= (VChargeAt V S) 0)
                                       (= (VCDischarge V S)
                                          (VChargeAt V (- S 1))))
                                  (and (= (VChargeAt V S)
                                          (- (VChargeAt V (- S 1)) (VCRate V)))
                                       (= (VCDischarge V S) (VCRate V))))))
                (implies (= (VFunctionAt V S) 3)
                         (and (= (VChargeAt V S) (VChargeAt V (- S 1)))
                              (= (VCFReg V S) (VChargeAt V (- S 1)))))))))

; stored charge at the end of the vehicle should be >= expected stored charge
(assert (forall ((V Int))
  (implies (and (>= V 1) (<= V 6)) (>= (VChargeAt V (VEndAt V)) (VChargeEnd V)))))

; Cases when the charged/discharged/capacity for frequency regulation is zero
(assert (forall ((V Int) (S Int))
  (implies (and (>= V 1) (<= V 6) (>= S 1) (<= S 8))
           (and (implies (= (VFunctionAt V S) 0)
                         (and (= (VCCharge V S) 0)
                              (= (VCDischarge V S) 0)
                              (= (VCFReg V S) 0)))
                (implies (= (VFunctionAt V S) 1)
                         (and (> (VCCharge V S) 0)
                              (= (VCDischarge V S) 0)
                              (= (VCFReg V S) 0)))
                (implies (= (VFunctionAt V S) 2)
                         (and (= (VCCharge V S) 0)
                              (> (VCDischarge V S) 0)
                              (= (VCFReg V S) 0)))
                (implies (= (VFunctionAt V S) 3)
                         (and (= (VCCharge V S) 0)
                              (= (VCDischarge V S) 0)
                              (> (VCFReg V S) 0)))))))

; Summation of the total charged/discharged/frequency regulation at each time slot
(assert (= (TotalCChargeAt 1)
   (+ (VCCharge 1 1) 
      (VCCharge 2 1)
      (VCCharge 3 1)
      (VCCharge 4 1)
      (VCCharge 5 1)
      (VCCharge 6 1))))
(assert (= (TotalCDischargeAt 1)
   (+ (VCDischarge 1 1)
      (VCDischarge 2 1)
      (VCDischarge 3 1)
      (VCDischarge 4 1)
      (VCDischarge 5 1)
      (VCDischarge 6 1))))
(assert (= (TotalCFRegAt 1)
   (+ (VCFReg 1 1)
      (VCFReg 2 1)
      (VCFReg 3 1)
      (VCFReg 4 1)
      (VCFReg 5 1)
      (VCFReg 6 1))))
(assert (= (TotalCChargeAt 2)
   (+ (VCCharge 1 2)
      (VCCharge 2 2)
      (VCCharge 3 2)
      (VCCharge 4 2)
      (VCCharge 5 2)
      (VCCharge 6 2))))
(assert (= (TotalCDischargeAt 2)
   (+ (VCDischarge 1 2)
      (VCDischarge 2 2)
      (VCDischarge 3 2)
      (VCDischarge 4 2)
      (VCDischarge 5 2)
      (VCDischarge 6 2))))
(assert (= (TotalCFRegAt 2)
   (+ (VCFReg 1 2)
      (VCFReg 2 2)
      (VCFReg 3 2)
      (VCFReg 4 2)
      (VCFReg 5 2)
      (VCFReg 6 2))))
(assert (= (TotalCChargeAt 3)
   (+ (VCCharge 1 3)
      (VCCharge 2 3)
      (VCCharge 3 3)
      (VCCharge 4 3)
      (VCCharge 5 3)
      (VCCharge 6 3))))
(assert (= (TotalCDischargeAt 3)
   (+ (VCDischarge 1 3)
      (VCDischarge 2 3)
      (VCDischarge 3 3)
      (VCDischarge 4 3)
      (VCDischarge 5 3)
      (VCDischarge 6 3))))
(assert (= (TotalCFRegAt 3)
   (+ (VCFReg 1 3)
      (VCFReg 2 3)
      (VCFReg 3 3)
      (VCFReg 4 3)
      (VCFReg 5 3)
      (VCFReg 6 3))))
(assert (= (TotalCChargeAt 4)
   (+ (VCCharge 1 4)
      (VCCharge 2 4)
      (VCCharge 3 4)
      (VCCharge 4 4)
      (VCCharge 5 4)
      (VCCharge 6 4))))
(assert (= (TotalCDischargeAt 4)
   (+ (VCDischarge 1 4)
      (VCDischarge 2 4)
      (VCDischarge 3 4)
      (VCDischarge 4 4)
      (VCDischarge 5 4)
      (VCDischarge 6 4))))
(assert (= (TotalCFRegAt 4)
   (+ (VCFReg 1 4)
      (VCFReg 2 4)
      (VCFReg 3 4)
      (VCFReg 4 4)
      (VCFReg 5 4)
      (VCFReg 6 4))))
(assert (= (TotalCChargeAt 5)
   (+ (VCCharge 1 5)
      (VCCharge 2 5)
      (VCCharge 3 5)
      (VCCharge 4 5)
      (VCCharge 5 5)
      (VCCharge 6 5))))
(assert (= (TotalCDischargeAt 5)
   (+ (VCDischarge 1 5)
      (VCDischarge 2 5)
      (VCDischarge 3 5)
      (VCDischarge 4 5)
      (VCDischarge 5 5)
      (VCDischarge 6 5))))
(assert (= (TotalCFRegAt 5)
   (+ (VCFReg 1 5)
      (VCFReg 2 5)
      (VCFReg 3 5)
      (VCFReg 4 5)
      (VCFReg 5 5)
      (VCFReg 6 5))))
(assert (= (TotalCChargeAt 6)
   (+ (VCCharge 1 6)
      (VCCharge 2 6)
      (VCCharge 3 6)
      (VCCharge 4 6)
      (VCCharge 5 6)
      (VCCharge 6 6))))
(assert (= (TotalCDischargeAt 6)
   (+ (VCDischarge 1 6)
      (VCDischarge 2 6)
      (VCDischarge 3 6)
      (VCDischarge 4 6)
      (VCDischarge 5 6)
      (VCDischarge 6 6))))
(assert (= (TotalCFRegAt 6)
   (+ (VCFReg 1 6)
      (VCFReg 2 6)
      (VCFReg 3 6)
      (VCFReg 4 6)
      (VCFReg 5 6)
      (VCFReg 6 6))))
(assert (= (TotalCChargeAt 7)
   (+ (VCCharge 1 7)
      (VCCharge 2 7)
      (VCCharge 3 7)
      (VCCharge 4 7)
      (VCCharge 5 7)
      (VCCharge 6 7))))
(assert (= (TotalCDischargeAt 7)
   (+ (VCDischarge 1 7)
      (VCDischarge 2 7)
      (VCDischarge 3 7)
      (VCDischarge 4 7)
      (VCDischarge 5 7)
      (VCDischarge 6 7))))
(assert (= (TotalCFRegAt 7)
   (+ (VCFReg 1 7)
      (VCFReg 2 7)
      (VCFReg 3 7)
      (VCFReg 4 7)
      (VCFReg 5 7)
      (VCFReg 6 7))))
(assert (= (TotalCChargeAt 8)
   (+ (VCCharge 1 8)
      (VCCharge 2 8)
      (VCCharge 3 8)
      (VCCharge 4 8)
      (VCCharge 5 8)
      (VCCharge 6 8))))
(assert (= (TotalCDischargeAt 8)
   (+ (VCDischarge 1 8)
      (VCDischarge 2 8)
      (VCDischarge 3 8)
      (VCDischarge 4 8)
      (VCDischarge 5 8)
      (VCDischarge 6 8))))
(assert (= (TotalCFRegAt 8)
   (+ (VCFReg 1 8)
      (VCFReg 2 8)
      (VCFReg 3 8)
      (VCFReg 4 8)
      (VCFReg 5 8)
      (VCFReg 6 8))))

; Constraints      
(assert (and (or (= (TotalCFRegAt 1) 0) (>= (TotalCFRegAt 1) 20))
     (or (= (TotalCDischargeAt 1) 0)
         (and (<= (TotalCDischargeAt 1) 40) (>= (TotalCDischargeAt 1) 10)))
     (or (= (TotalCChargeAt 1) 0) (<= (TotalCChargeAt 1) 70))))
(assert (and (or (= (TotalCFRegAt 2) 0) (>= (TotalCFRegAt 2) 20))
     (or (= (TotalCDischargeAt 2) 0)
         (and (<= (TotalCDischargeAt 2) 40) (>= (TotalCDischargeAt 2) 10)))
     (or (= (TotalCChargeAt 2) 0) (<= (TotalCChargeAt 2) 70))))
(assert (and (or (= (TotalCFRegAt 3) 0) (>= (TotalCFRegAt 3) 20))
     (or (= (TotalCDischargeAt 3) 0)
         (and (<= (TotalCDischargeAt 3) 50) (>= (TotalCDischargeAt 3) 10)))
     (or (= (TotalCChargeAt 3) 0) (<= (TotalCChargeAt 3) 60))))
(assert (and (or (= (TotalCFRegAt 4) 0) (>= (TotalCFRegAt 4) 35))
     (or (= (TotalCDischargeAt 4) 0)
         (and (<= (TotalCDischargeAt 4) 40) (>= (TotalCDischargeAt 4) 10)))
     (or (= (TotalCChargeAt 4) 0) (<= (TotalCChargeAt 4) 40))))
(assert (and (or (= (TotalCFRegAt 5) 0) (>= (TotalCFRegAt 5) 25))
     (or (= (TotalCDischargeAt 5) 0)
         (and (<= (TotalCDischargeAt 5) 50) (>= (TotalCDischargeAt 5) 20)))
     (or (= (TotalCChargeAt 5) 0) (<= (TotalCChargeAt 5) 50))))
(assert (and (or (= (TotalCFRegAt 6) 0) (>= (TotalCFRegAt 6) 35))
     (or (= (TotalCDischargeAt 6) 0)
         (and (<= (TotalCDischargeAt 6) 50) (>= (TotalCDischargeAt 6) 10)))
     (or (= (TotalCChargeAt 6) 0) (<= (TotalCChargeAt 6) 50))))
(assert (and (or (= (TotalCFRegAt 7) 0) (>= (TotalCFRegAt 7) 20))
     (or (= (TotalCDischargeAt 7) 0)
         (and (<= (TotalCDischargeAt 7) 40) (>= (TotalCDischargeAt 7) 10)))
     (or (= (TotalCChargeAt 7) 0) (<= (TotalCChargeAt 7) 60))))
(assert (and (or (= (TotalCFRegAt 8) 0) (>= (TotalCFRegAt 8) 20))
     (or (= (TotalCDischargeAt 8) 0)
         (and (<= (TotalCDischargeAt 8) 40) (>= (TotalCDischargeAt 8) 10)))
     (or (= (TotalCChargeAt 8) 0) (<= (TotalCChargeAt 8) 70))))


(assert (= (+ (- (+ (* (TotalCDischargeAt 1) 1) (* (TotalCFRegAt 1) 1))
          (* (TotalCChargeAt 1) 1))
       (- (+ (* (TotalCDischargeAt 2) 1) (* (TotalCFRegAt 2) 1))
          (* (TotalCChargeAt 2) 1))
       (- (+ (* (TotalCDischargeAt 3) 1) (* (TotalCFRegAt 3) 1))
          (* (TotalCChargeAt 3) 1))
       (- (+ (* (TotalCDischargeAt 4) 2) (* (TotalCFRegAt 4) 2))
          (* (TotalCChargeAt 4) 2))
       (- (+ (* (TotalCDischargeAt 5) 2) (* (TotalCFRegAt 5) 1))
          (* (TotalCChargeAt 5) 2))
       (- (+ (* (TotalCDischargeAt 6) 2) (* (TotalCFRegAt 6) 2))
          (* (TotalCChargeAt 6) 2))
       (- (+ (* (TotalCDischargeAt 7) 1) (* (TotalCFRegAt 7) 1))
          (* (TotalCChargeAt 7) 1))
       (- (+ (* (TotalCDischargeAt 8) 1) (* (TotalCFRegAt 8) 1))
          (* (TotalCChargeAt 8) 1)))
    Total))


(assert (>= Total 500))

(check-sat)
(get-model)

我想知道我的形式化是否效率不高或者我要解决的问题很复杂。

4

1 回答 1

4

不，一般来说，Z3 不会在不满意的情况下花费更长的时间。这是您的问题的一个特殊特征。实际上，对于包含量词的问题，Z3 通常需要更长的时间才能返回sat。对于包含量词的问题，Z3 可能经常返回unknown可满足的实例。Z3 指南描述了许多类别的问题（包含量词），其中 Z3 能够返回sat可满足的实例。在您的问题中，您仅使用有界量词。因此，您处于 Z3 支持的可判定片段中。

Z3 中用于处理量词的启发式算法并未针对仅使用有界量词的问题进行调整。在我的机器上，我只使用选项就获得了 4 倍的时间加速RELEVANCY=0。您还可以通过(set-option :relevancy 0)在 SMT2 文件中添加命令来设置此选项。在编程 API 中，您可以在创建逻辑上下文时设置此选项。

其次，量词并不是真正需要对您的问题进行编码。您可以使用编程 API 轻松生成所有需要的实例。这是一个使用 Python API 的小例子（也在http://rise4fun.com/Z3Py/yzcX）。

VFunctionAt = Function('VFunctionAt', IntSort(), IntSort(), IntSort())

s = Solver()
s.add([VFunctionAt(V,S) >= 0 for V in range(1, 5) for S in range(1, 9)])
print s

在这个例子中，我本质上是在编码forall V in [1,4] S in [1,8] VFunctionAt(V,S) >= 0. 通过扩展量词，您可以在很多方面帮助 Z3：它不必在搜索期间扩展量词；它将对问题使用正确的启发式方法（因为问题将是无量词的）；它不必检查 Z3 正在构建的模型/解决方案是否真的满足量化公式。

未来，我们计划在 Z3 中添加对检测这种所有量词有界的问题实例的支持，并自动为用户执行此转换。

于 2012-10-06T16:21:49.710 回答