表示 SMT-LIB 中的时间约束

我试图在 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)
)

一些实用宏被定义用于时间和持续时间算术以及表达关系。例如，使用我们定义的一些辅助宏长于, 比短 and 持续时间相等如下：

(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的在线证明和我的代码可以找到here。我还没有尝试过其他 SMT 求解器。

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

Thanks!

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

Also, mathematically, the integer theories are harder than their real counterparts. For example "n = pq, solve for p" is trivial if n, p, and q are reals, but if they're integers then it's integer factoring, which is hard. Similarly xⁿ + yⁿ = zⁿ, n > 2 is easy to solve in the reals, but in the integers, that's Fermat's last theorem. These examples are nonlinear, but I claim you're better-off to be in QF_LRA than QF_LIA, if you consider that the techniques used to solve QF_LRA are taught to middle-school and high-school students. Time is closer to a real number than it is to a bunch of integers, anyway.

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