与饱和结果相比，Z3 是否需要更长的时间才能给出未饱和结果？答案

【问题标题】：Does Z3 take a longer time to give an unsat result compared to a sat result?与饱和结果相比，Z3 是否需要更长的时间才能给出未饱和结果？
【发布时间】：2012-09-30 06:08:09
【问题描述】：

根据我的经验，在较大型号的情况下，我发现与饱和情况相比，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

(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 票才能重新开放。
@LeonardodeMoura：我也投票决定重新开放。您应该标记该问题并向版主解释为什么应该打开该问题。由于完全重复，一个新问题可能会再次关闭。
@LeonardodeMoura：我使用 .NET API (V3) 编写了程序。我使用 .ToString() 函数打印了 SMT-LIB 等效（没有断言）代码。是否有任何函数可用于获取我的程序的确切 SMT-LIB 等效代码（包括声明）？我的程序有大约 500 行代码。如果可能的话，我可以给你我的代码（连同输入文件）。

标签： z3

【解决方案1】：

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

Z3 中用于处理量词的启发式算法并未针对仅使用有界量词的问题进行调整。在我的机器上，我只使用选项RELEVANCY=0 就获得了 4 倍的时间加速。您还可以通过在 SMT2 文件中添加命令 (set-option :relevancy 0) 来设置此选项。在编程 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 中添加支持，以检测这种所有量词都有界的问题实例，并为用户自动执行此转换。

【讨论】：

我在我的问题中包含了另一个示例，其中包含 6 辆车（仅比前面的示例多 2 辆）。从这个例子中，您将能够比较性能如何恶化，尤其是在结果不满意的情况下。有什么办法可以让性能更好吗？然而，早些时候我也编码了类似的没有量词的问题。尽管我获得了更好的性能，但与饱和案例相比，未饱和案例仍然需要更多时间。我很快就会在没有量词的情况下对这个当前的问题进行编码。我会让你知道表现。谢谢。
为了更好的性能，我建议选择RELEVANCY=0。顺便说一句，我报告的加速是针对未满足的情况。根据您前段时间发布的日志，我相信您使用的是旧版本的 Z3。我强烈建议您使用更新的版本。最新版本以源代码形式提供，地址为z3.codeplex.com。 Z3 4.1 二进制版本也可以在 Z3 主页上找到。将来，我们将在z3.codeplex.com 包含新的 Windows 二进制版本。
我在没有使用任何量词的情况下对我的问题进行了编码。尽管性能有所提高，但对于 unsat 案例仍然需要很长时间。对于 10 辆或更多车辆，等待时间太长。如果你愿意，我可以和你分享我的整个项目，以便你验证。
是的，看看这个有 10 辆车的例子会很棒。
8车问题请执行以下SMT-LIB V2代码：(dl.dropbox.com/u/35018736/SMT_LIB_Program_8.txt)。这里，预期的验证结果是“不满意”。如果需要，您可以在此处更改值：“(assert (>= Total 1200))”以获得可满足的情况（例如，“(assert (>= Total 600))”）。您可以在以下链接中找到完整的 .NET 项目：(dropbox.com/sh/s7vcn58mpg8cycq/Vlm7zXbx-P/Prog_V2G)。有4、6、8、128辆车的输入文件。您可以更改最低收入约束（输入文件的最后一行）以查看不同的行为。