在 SMT-LIB 中表示时间约束
Representing temporal constraints in SMT-LIB
我试图在 SMT-LIB 中表示时间约束以检查它们的可满足性。我正在寻找有关我所采取的方向的反馈。我对 SMT-LIB 比较陌生，非常感谢您的投入。
我的限制是关于事件的时间和持续时间。例如，考虑以下用自然语言给出的约束：
John 在 13:03:41 开始写一篇文章，他花了 20 分钟才完成。
写完后，他查看邮件，花了他40多分钟。
查看邮件后，他给妻子打了电话。
他在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)
)
其余定义可在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)
一些疑问和问题：
在设计方面，我很想知道这是否是 SMT-LIB 中问题的合理建模。
要在此处添加一些注释：(A) 我决定使用数组来表示时间和持续时间对象，因为它们有助于对这些概念的内部字段（小时、分钟、秒、纳秒）进行分组).也可以使用单个整数。 (B) 我非常依赖宏（define-fun ...），这可能会使约束有点复杂，但我不知道还有什么可以用来达到所需的表达力和清晰度水平当前代码有。 (C) 目前没有限制时间字段的约束，所以分钟字段的值，例如可以是78。应该添加断言，限制秒为59，分钟为59，小时为23 ，但我没有找到一种优雅的方式来做到这一点。
我假设我在 FOL 的可判定片段中 - QF_LIA - 因为所有约束都是使用整数常量上的线性函数声明的。不过，我试过运行the attached code through Z3 and even after 40 minutes of running locally on average computer it still doesn't return with a resolution (sat/unsat). I actually don't know if it can solve the problem at all. It's possible that my assumption of being in QF-LIA is wrong and it's also possible that Z3 struggles with this type of constraints. I can add that When I tried simpler constraints Z3 managed to reach a resolution but I noticed that the models it generated were very complicated with lots of internal structures. Could someone please give me some ideas to investigate here? Z3's online prover with my code can be found here。我还没有尝试过其他 SMT 求解器。
我不知道有平行作品试图在 SMT-LIB 中定义这种类型的时间约束。我非常感谢对现有作品的引用。
谢谢！
我喜欢你的方法，但我认为你定义自己的排序，尤其是使用数组理论，使情况过于复杂。
此外，从数学上讲，整数理论比它们的真实对应物更难。例如“n = pq，求解 p”如果 n, p 和 q 是实数，但如果它们是整数，那么它就是整数因式分解，这很难。同样 xn + yn = zn, 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))
我试图在 SMT-LIB 中表示时间约束以检查它们的可满足性。我正在寻找有关我所采取的方向的反馈。我对 SMT-LIB 比较陌生，非常感谢您的投入。
我的限制是关于事件的时间和持续时间。例如，考虑以下用自然语言给出的约束：
John 在 13:03:41 开始写一篇文章，他花了 20 分钟才完成。
写完后，他查看邮件，花了他40多分钟。
查看邮件后，他给妻子打了电话。
他在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)
)
其余定义可在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)
一些疑问和问题：
在设计方面，我很想知道这是否是 SMT-LIB 中问题的合理建模。
要在此处添加一些注释：(A) 我决定使用数组来表示时间和持续时间对象，因为它们有助于对这些概念的内部字段（小时、分钟、秒、纳秒）进行分组).也可以使用单个整数。 (B) 我非常依赖宏（define-fun ...），这可能会使约束有点复杂，但我不知道还有什么可以用来达到所需的表达力和清晰度水平当前代码有。 (C) 目前没有限制时间字段的约束，所以分钟字段的值，例如可以是78。应该添加断言，限制秒为59，分钟为59，小时为23 ，但我没有找到一种优雅的方式来做到这一点。
我假设我在 FOL 的可判定片段中 - QF_LIA - 因为所有约束都是使用整数常量上的线性函数声明的。不过，我试过运行the attached code through Z3 and even after 40 minutes of running locally on average computer it still doesn't return with a resolution (sat/unsat). I actually don't know if it can solve the problem at all. It's possible that my assumption of being in QF-LIA is wrong and it's also possible that Z3 struggles with this type of constraints. I can add that When I tried simpler constraints Z3 managed to reach a resolution but I noticed that the models it generated were very complicated with lots of internal structures. Could someone please give me some ideas to investigate here? Z3's online prover with my code can be found here。我还没有尝试过其他 SMT 求解器。
我不知道有平行作品试图在 SMT-LIB 中定义这种类型的时间约束。我非常感谢对现有作品的引用。
谢谢！
我喜欢你的方法，但我认为你定义自己的排序，尤其是使用数组理论，使情况过于复杂。
此外，从数学上讲，整数理论比它们的真实对应物更难。例如“n = pq，求解 p”如果 n, p 和 q 是实数，但如果它们是整数，那么它就是整数因式分解，这很难。同样 xn + yn = zn, 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))