Does Z3 take a longer time to give an unsat result compared to a sat result?

Question

From my experiences, in case of larger models, I found that Z3 takes a very longer time to give an unsat result compared to the sat cases. Even sometimes Z3 is running an infinite time without giving no answer. In the following I give an example of such cases. [Though I used .NET API for formalization, I am writing here the equivalent SMT-LIB 2 code.]

(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)

In my formalization, I mainly used uninterpreted functions. In this example I only shows 4 vehicles (1<=V<= 4) and 4 time slots (1<=S<=4). Here, in the cases of unsat results, the solver takes almost 40 times more time than the cases of sat results. When we increase the size, e.g., 6 vehicles and 8 slots (as shown below), and set the minimum benefit (i.e., Total) to a larger value (e.g., 600), it keeps running for a long time without giving any answer (an unsat result was expecting). However, in the sat cases (lower minimum benefit), Z3 takes few seconds. Due to a small increase in the number of vehicles/slots the performance reduces significantly in both of the sat and unsat cases, though performance in the unsat cases is horrible.

(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)

I am wondering whether my formalization is not efficient or the problem I am addressing is complex.

Answer 1

No, in general, Z3 does not take longer on unsatisfiable instances. This is a particular characteristic of your problem. Actually, for problems containing quantifiers, Z3 usually takes much longer to return sat. For problems containing quantifiers, Z3 may very often return unknown for satisfiable instances. The Z3 guide describes many classes of problems (containing quantifiers) where Z3 is capable of returning sat for satisfiable instances. In your problem, you use only bounded quantifiers. Thus, you are in decidable fragment supported by Z3.

The heuristics for handling quantifiers in Z3 are not tuned for problems that use only bounded quantifiers. On my machine, I got a 4x time speedup just using the option RELEVANCY=0. You can also set this option by adding the command (set-option :relevancy 0) in your SMT2 file. In the programmatic API, you can set this option when you create the logical context.

Second, quantifiers are not really needed to encode your problem. You can easily generate all needed instances using the programmatic API. Here is a small example using the Python API (also at 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

In this example, I'm essentially encoding forall V in [1,4] S in [1,8] VFunctionAt(V,S) >= 0. By expanding the quantifiers, you are helping Z3 in many ways: it will not have to expand the quantifiers during the search; it will use the right heuristics for the problem (since the problem will be quantifier free); it will not have to check whether the quantified formulas were really satisfied or not by the model/solution being constructed by Z3.

In the future, we plan to add support in Z3 for detecting this kind of problem instance where all quantifiers are bounded, and perform this transformation automatically for the user.