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.

Can you post an example exhibiting the behaviour? Otherwise, it's too difficult to answer your question. — pad, Sep 30 '12 at 08:51
I have revised the question and gave an example. I hope, this will help you to give an answer to my question. — Ashiq, Oct 02 '12 at 11:36
Could you provide the complete example? I can't execute it on my machine since the declarations are missing. Regarding the "close" status, I think you should create another question. I voted it to be reopen, but we still need another 4 votes to reopen it. — Leonardo de Moura, Oct 03 '12 at 22:08
@LeonardodeMoura: I voted to reopen too. You should flag the question and explain to moderators why the question should be opened. A new question is likely to be closed again due to exact duplication. — pad, Oct 04 '12 at 05:41
@LeonardodeMoura: I wrote the program using .NET API (V3). I printed the SMT-LIB equivalent (without assert) code using .ToString() function. Is there any function that I can use to get the exact SMT-LIB equivalent code (including the declarations) of my program? My program has around 500 lines of code. If it is possible, I can give you my code (along with the input file). — Ashiq, Oct 05 '12 at 07:12
From the .Net API, you can create a log of the interaction between your application and Z3. If you are using .NET API (V3), you should use `Z3Log.Open("z3.log")`. You have to invoke it before any other API call. We can replay the log in our machines. — Leonardo de Moura, Oct 05 '12 at 15:45
I have updated my question. The example is now complete (SMT-LIB 2 code). I hope, now you will be able to give me an answer. If you need, I can also give another example with 6 or more vehicles. However, my question is still "closed". — Ashiq, Oct 06 '12 at 09:03

score 4 · Accepted Answer · answered Oct 06 '12 at 16:21

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.

I have included another example with 6 vehicles (only 2 more than the earlier example) in my question. From this example, you will be able to compare how the performance, especially in case of unsat result, deteriorates. Is there any way, that can make the performance better? However, earlier I also encoded similar kind of problems without quantifiers. Though I received better performance, the unsat cases still took more time compared to the sat cases. I will soon encode this current problem without quantifier. I will let you know the performance. Thanks. — Ashiq, Oct 07 '12 at 02:21
For better performance, I suggested the option `RELEVANCY=0`. BTW, the speedups that I reported were for the unsat cases. Based on the log you posted a while ago, I believe you are using an old version of Z3. I strongly suggest you move to more recent versions. The latest version is available in source code form at http://z3.codeplex.com. Z3 4.1 binary release is also available in the Z3 homepage. In the future, we will include new binary releases for Windows at http://z3.codeplex.com. — Leonardo de Moura, Oct 07 '12 at 15:34
I have encoded my problem without any use of quantifiers. Though performance has been improved, it still takes a very long time for unsat cases. For 10 or more vehicles, it is too long to wait. If you like, I can share my whole project with you, so that you can verify. — Ashiq, Oct 12 '12 at 10:28
Yes, it would be great to take a look in the example with 10 vehicles. — Leonardo de Moura, Oct 14 '12 at 20:10
Please execute the following SMT-LIB V2 code for a problem of 8 vehicles: (https://dl.dropbox.com/u/35018736/SMT_LIB_Program_8.txt). Here, the expected verification result is 'unsatisfiable'. If you need, you can change the value here: "(assert (>= Total 1200))" for a satisfiable case (e.g., "(assert (>= Total 600))"). You will find the full .NET project in the following link: (https://www.dropbox.com/sh/s7vcn58mpg8cycq/Vlm7zXbx-P/Prog_V2G). There are input files for 4, 6, 8, 128 vehicles. You can change minimum revenue constraint (the last line of the input file) to see different behaviors. — Ashiq, Oct 21 '12 at 09:11

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

1 Answers1

Linked