表示SMT-LIB中的时间约束 [英] Representing temporal constraints in SMT-LIB

问题描述

我试图在SMT-LIB中表示时间约束，以便检查其可满足性.我正在寻找有关我所走方向的反馈.我是SMT-LIB的新手，我将不胜感激.

我的约束条件是事件的时间和持续时间.例如，请考虑以下自然语言给出的约束:

1. John从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)
)

字母是使用宏定义的，允许我们检索特定的度量，例如:

(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)我决定使用数组来表示时间和持续时间对象，因为它们有助于对这些概念的内部字段(小时，分钟，秒，nanos)进行分组.单个整数也可以使用. (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中定义这种类型的时间约束的并行工作.我非常感谢对现有作品的引用.

谢谢！

解决方案

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

此外，在数学上，整数理论比真实的理论更难.例如，如果 n ， p 和 q 是实数，但是如果它们是整数，则它是整数分解，这很难.类似地， 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))

I'm trying to represent temporal constraints in SMT-LIB in order to check their satisfiability. I'm looking for feedback on the direction I'm taking. I'm relatively new to SMT-LIB and I'll highly appreciate inputs.

The constraints that I have are about the time and duration of events. For example, consider the following constraints given in natural language:

1. John started writing an essay at 13:03:41, and it took him 20 min to complete it.

2. After writing, he checked his emails, which took him more than 40 min.

3. After checking his emails, he phoned his wife.

4. He phoned his wife after 14:00:00.

It is easy to see that this set of constraints is staisfiable and I'm trying to deduce that using an SMT solver.

To have some sore of encapsulation for the concepts of time and duration I defined new sorts that represent them in arrays. Some macros were defined for acting as constructions:

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

Getters are defined using macros and allow us to retrieve specific measures, for instance:

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

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

Some utility macros were defined for time and duration arithmetic and for expressing relations. For example, using some helper macros we define isLongerThan, isShorterThan and isEqualDuration as follows:

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

The rest of the definitions can be found in this file.

Based on this I can express the constraints by a set of assertions:

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

Some questions and problems:

1. Design-wise, I'd be interested to know whether this is a reasonable modeling of the problem in SMT-LIB.

2. Some notes to add here: (A) I decided to use arrays to represent the time and duration objects since they help to group the internal fields of these concepts (hours, minutes, seconds, nanos). Individual integers could be used just as well. (B) I'm relying on macros (define-fun ...) very heavily, and this could make the constraints a bit complicated, but I don't know what else could be used for reaching the required level of expressiveness and clarity that the current code has. (C) Currently there are no constraints that limit the time fields, so the value of the minutes field, for example, can be 78. Assertions should be added that restrict the seconds to 59, the minutes to 59, and the hours to 23, but I didn't find an elegant way to do that.

3. I assume that I'm in a decidable fragment of FOL - QF_LIA - since all constraints are declared using linear functions over integer constants. However, I tried to run 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. I haven't tried other SMT solvers yet.

4. I'm unaware of parallel works that try to define temporal constraints of this type in SMT-LIB. I'd really appreciate references to existing works.

Thanks!

解决方案

I like your approach, but I think your over-complicating the situation by defining your own sorts, and especially by using an array theory.

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.

In my experience with SMT solvers in general and Z3 in particular, you're better off to use a simpler theory. It will permit Z3 to use its most powerful internal solvers. If you use more sophisticated theories like arrays, you might get a spectacular result, or you might find that the solver times out and you have no idea why, as was the case with your proposed solution.

It's not as nice from a software engineering point of view, but mathematically I recommend the following simple solution to the problem you posed, where all times are represented as real numbers, in terms of the number of seconds since midnight on the day of interest:

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

Both Z3 and CVC4 quickly find a solution:

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中的时间约束的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！