0

私の経験から、より大きなモデルの場合、Z3は、satの場合と比較して、unsatの結果を出すのに非常に長い時間がかかることがわかりました。時々Z3は答えを出さずに無限の時間を実行しています。以下にそのような場合の例を示します。[形式化には.NETAPIを使用しましたが、ここでは同等のSMT-LIB2コードを記述しています。]

(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）のみを示しています。ここで、不飽和の結果の場合、ソルバーは、飽和の結果の場合のほぼ40倍の時間がかかります。サイズを大きくして（たとえば、6台の車両と8つのスロット（以下に示す）、最小のメリット（つまり、合計）をより大きな値（たとえば、600）に設定すると、何も答えずに長時間実行し続けます。 （不満の結果が予想されていました）。ただし、satの場合（最小のメリットが低い）、Z3には数秒かかります。車両/スロットの数がわずかに増加したため、土のない場合のパフォーマンスはひどいものですが、土の場合と土のない場合の両方でパフォーマンスが大幅に低下します。

(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 に答える