在 SMT-LIB 中表示时间约束

Question

我试图在 SMT-LIB 中表示时间约束，以检查它们的可满足性。我正在寻找有关我正在采取的方向的反馈。我对 SMT-LIB 比较陌生，我非常感谢输入。

我的限制是关于事件的时间和持续时间。例如，考虑以下自然语言中给出的约束：

1. 约翰从 13:03:41 开始写一篇文章，他花了 20 分钟才完成。

2. 写完之后，他检查了他的电子邮件，这花了他 40 多分钟。

3. 查完邮件后，他给妻子打了电话。

4. 14:00:00后他给妻子打了电话。

很容易看出这组约束是可稳定的，我正在尝试使用 SMT 求解器推断出这一点。

为了对时间和持续时间的概念进行一些封装，我定义了用数组表示它们的新类型。一些宏被定义为用作结构：

(define-sort Time () (Array Int Int))
(define-fun new_time_ns ((hours Int) (minutes Int) (seconds Int) (nanos Int)) Time
    (store (store (store (store ((as const (Array Int Int)) 0) 1 hours) 2 minutes) 3 seconds) 4 nanos)
)
(define-sort Duration () (Array Int Int))
(define-fun new_duration_ns ((seconds Int) (nanos Int)) Duration
    (store (store ((as const (Array Int Int)) 0) 1 seconds) 2 nanos)
)

Getter 是使用宏定义的，并允许我们检索特定的度量，例如：

(define-fun getDurationSecond ((d Duration)) Int
  (select d 1)
)

(define-fun getDurationNano ((d Duration)) Int
  (select d 2)
)

为时间和持续时间算术以及表达关系定义了一些实用宏。例如，使用一些辅助宏，我们定义isLongerThan、isShorterThan和isEqualDuration 如下：

(define-fun cmpInt ((i1 Int) (i2 Int)) Int
  (ite (< i1 i2) -1 (ite(> i1 i2) 1 0))
) 

(define-fun cmpDuration ((d1 Duration) (d2 Duration)) Int
  (ite (= (cmpInt (getDurationSecond d1) (getDurationSecond d2)) 0) 
    (ite (= (cmpInt (getDurationNano d1) (getDurationNano d2)) 0)
    0
    (cmpInt (getDurationNano d1) (getDurationNano d2)))
  (cmpInt (getDurationSecond d1) (getDurationSecond d2)))
)  

(define-fun isLongerThan ((d1 Duration) (d2 Duration)) Bool
  (> (cmpDuration d1 d2) 0)
)

(define-fun isShorterThan ((d1 Duration) (d2 Duration)) Bool
  (< (cmpDuration d1 d2) 0)
)

(define-fun isEqualDuration ((d1 Duration) (d2 Duration)) Bool
  (= (cmpDuration d1 d2) 0)
)

其余的定义可以在这个文件中找到。

基于此，我可以通过一组断言来表达约束：

(declare-const write_start Time)
(declare-const write_end Time)
(declare-const write_duration Duration)

(declare-const check_start Time)
(declare-const check_end Time)
(declare-const check_duration Duration)

(declare-const phone_start Time)

(assert (= write_start (new_time_ns 13 03 41 0)))  ; the writing started at 13:03:41
(assert (= write_duration (new_duration 1200)))    ; the writing took 20 min (1200 sec).
(assert (= write_end (plusDuration write_start write_duration)))

(assert (isAfter check_start write_end))                   ; the check started after the writing
(assert (isLongerThan check_duration (new_duration 2400))) ; the check took more than 40 min
(assert (= check_end (plusDuration check_start check_duration)))

(assert (isAfter phone_start check_end))                   ; he phoned after the check
(assert (isAfter phone_start (new_time_ns 14 00 00 0)))    ; it was after 14:00:00

(check-sat)

一些问题和问题：

1. 在设计方面，我很想知道这是否是 SMT-LIB 中问题的合理建模。

2. 这里要添加一些注释：(A) 我决定使用数组来表示时间和持续时间对象，因为它们有助于对这些概念的内部字段（小时、分钟、秒、纳秒）进行分组。也可以使用单个整数。(B) 我非常依赖宏（define-fun ...），这可能会使约束有点复杂，但我不知道还有什么可以用来达到所需的表现力和清晰度水平当前代码具有的。(C) 目前没有限制时间字段的约束，所以分钟字段的值，例如，可以是 78。应该添加断言，限制秒为 59，分钟为 59，小时为 23 ，但我没有找到一种优雅的方式来做到这一点。

3. 我假设我处于 FOL 的可判定片段 - QF_LIA - 因为所有约束都是使用整数常量上的线性函数声明的。但是，我尝试通过 Z3运行附加的代码，即使在普通计算机上本地运行 40 分钟后，它仍然没有以分辨率（sat/unsat）返回。我实际上不知道它是否可以解决问题。有可能我在 QF-LIA 中的假设是错误的，Z3 也可能在这种类型的约束下挣扎。我可以补充一点，当我尝试更简单的约束时，Z3 设法达到了一个分辨率，但我注意到它生成的模型非常复杂，有很多内部结构。有人可以给我一些想法在这里进行调查吗？Z3'. 我还没有尝试过其他 SMT 求解器。

4. 我不知道尝试在 SMT-LIB 中定义这种类型的时间约束的并行工作。我非常感谢对现有作品的引用。

谢谢！

Answer 1

我喜欢你的方法，但我认为你通过定义自己的排序，尤其是使用数组理论，使情况过于复杂。

此外，在数学上，整数理论比真正的对应物更难。例如，如果n、p和q是实数，则“ n = pq , solve for p ”是微不足道的，但如果它们是整数，那么它就是整数因式分解，这很困难。类似地，x ⁿ + y ⁿ = z ⁿ , n > 2在实数中很容易求解，但在整数中，这是费马大定理。这些例子是非线性的，但我认为你在 QF_LRA 中比在 QF_LIA 中更好，如果你考虑到用于解决 QF_LRA 的技术是教给初中和高中学生的。无论如何，时间更接近于实数而不是一堆整数。

根据我对 SMT 求解器的总体经验，尤其是 Z3，您最好使用更简单的理论。它将允许 Z3 使用其最强大的内部求解器。如果您使用更复杂的理论，如数组，您可能会得到一个惊人的结果，或者您可能会发现求解器超时而您不知道为什么，就像您提出的解决方案一样。

从软件工程的角度来看，这不是很好，但从数学上讲，我建议使用以下简单解决方案来解决您提出的问题，其中所有时间都表示为实数，根据感兴趣的当天午夜起的秒数：

; Output all real-valued numbers in decimal-format.
(set-option :pp.decimal true)

; Convenience function for converting hh:mm:ss formatted times to seconds since midnight.
(define-fun time_hms ((hour Real) (minute Real) (second Real)) Real
    (+ (+ (* 3600.0 hour) (* 60.0 minute)) second)
)

; Convenience function for converting durations in minutes to seconds.
(define-fun duration_m ((minute Real)) Real
    (* 60.0 minute)
)

; Variable declarations. Durations are in seconds. Times are in seconds since midnight.
(declare-fun write_start () Real)
(declare-fun write_end () Real)
(declare-fun write_duration () Real)
(declare-fun check_start () Real)
(declare-fun check_end () Real)
(declare-fun check_duration () Real)
(declare-fun phone_start () Real)

; Constraints.

; 1. John started writing an essay at 13:03:41, and it took him 20 min to complete it.
(assert (= write_start (time_hms 13 03 41)))
(assert (= write_duration (duration_m 20)))
(assert (= write_end (+ write_start write_duration)))

; 2. After writing, he checked his emails, which took him more than 40 min.
(assert (> check_start write_end))
(assert (> check_duration (duration_m 40)))
(assert (= check_end (+ check_start check_duration)))

; 3. After checking his emails, he phoned his wife.
(assert (> phone_start check_end))

; 4. He phoned his wife after 14:00:00.
(assert (> phone_start (time_hms 14 00 00)))

(check-sat)
(get-value (write_start write_duration write_end check_start check_end check_duration phone_start))
(exit)

Z3 和 CVC4 都很快找到了解决方案：

sat
((write_start 47021.0)
 (write_duration 1200.0)
 (write_end 48221.0)
 (check_start 48222.0)
 (check_end 50623.0)
 (check_duration 2401.0)
 (phone_start 50624.0))