Representing temporal constraints in SMT-LIB

Question

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!

Answer 1

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