在 SMT-LIB 中表示时间约束

Question

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

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

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

2. 写完后，他查了邮件，花了40多分钟。

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

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

很容易看出，这组约束是 staisfiable，我正在尝试使用 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 em>如下：

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

其余定义见this file。

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

(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 运行the attached code，即使在普通计算机上本地运行 40 分钟后，它仍然没有返回分辨率（sat/unsat）。我实际上不知道它是否可以解决问题。我对 QF-LIA 的假设可能是错误的，Z3 也可能在这种类型的限制中挣扎。我可以补充一点，当我尝试更简单的约束时，Z3 设法达到了一个分辨率，但我注意到它生成的模型非常复杂，有很多内部结构。有人可以给我一些想法来在这里调查吗？ Z3 的在线证明器和我的代码可以在here 找到。我还没有尝试过其他 SMT 求解器。

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

谢谢！

Answer 1

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

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

根据我对 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))