与 sat 结果相比，Z3 是否需要更长的时间才能给出 unsat 结果? [英] Does Z3 take a longer time to give an unsat result compared to a sat result?
本文介绍了与 sat 结果相比，Z3 是否需要更长的时间才能给出 unsat 结果?的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
根据我的经验，在较大模型的情况下，我发现与 sat 情况相比，Z3 需要更长的时间才能给出不满足的结果.甚至有时 Z3 会无限运行而不给出任何答复.下面我举一个这样的例子.[虽然我使用 .NET API 进行形式化，但我在这里编写了等效的 SMT-LIB 2 代码.]
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)
在我的形式化中，我主要使用未解释的函数.在这个例子中，我只显示了 4 辆车(1<=V<=4)和 4 个时隙(1<=S<=4).在这里，在 unsat 结果的情况下，求解器花费的时间几乎是 sat 结果的 40 倍.当我们增加大小，例如6辆车和8个插槽(如下图)，并将最小收益(即Total)设置为更大的值(例如600)时，它会持续运行很长时间而不给出任何答案(期待一个不满意的结果).然而，在 sat 情况下(较低的最小收益)，Z3 需要几秒钟.由于车辆/插槽数量的小幅增加，sat 和 unsat 情况下的性能显着下降，尽管 unsat 情况下的性能很糟糕.
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.
推荐答案
不，一般来说，Z3 不会在不可满足的实例上花费更长的时间.这是您的问题的一个特殊特征.实际上，对于包含量词的问题，Z3 通常需要更长的时间来返回 sat.对于包含量词的问题，Z3 可能经常为可满足的实例返回 unknown.Z3 指南 描述了许多类别的问题(包含量词)，其中 Z3 能够返回 sat 用于可满足的实例.在您的问题中，您仅使用有界量词.因此，您处于 Z3 支持的可判定片段中.
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.
Z3 中处理量词的启发式方法并未针对仅使用有界量词的问题进行调整.在我的机器上，我只使用选项 RELEVNCY=0 就获得了 4 倍的时间加速.您还可以通过在 SMT2 文件中添加命令 (set-option :relevancy 0) 来设置此选项.在编程 API 中，您可以在创建逻辑上下文时设置此选项.
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.
其次，对您的问题进行编码并不真正需要量词.您可以使用编程 API 轻松生成所有需要的实例.这是一个使用 Python API 的小例子(也在 http://rise4fun.com/Z3Py/yzcX).
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
在这个例子中，我本质上是在 [1,8] VFunctionAt(V,S) >= 0 中编码 forall V in [1,4] S in [1,8].通过扩展量词，您在很多方面都在帮助 Z3:它不必在搜索过程中扩展量词；它将对问题使用正确的启发式方法(因为问题将是无量词的)；无需检查 Z3 构建的模型/解决方案是否真正满足量化公式.
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.
未来，我们计划在 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.
这篇关于与 sat 结果相比，Z3 是否需要更长的时间才能给出 unsat 结果?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
查看全文
