Представление временных ограничений в SMT-LIB

Question

Я пытаюсь представить временные ограничения в 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) 
) 

Геттерз определяются с помощью макросов и позволяют получить конкретные меры, например:

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

Некоторые вопросы и проблемы:

1. Дизайн-мудрый, мне было бы интересно узнать, является ли это является разумным моделированием проблемы в SMT-LIB.

2. Некоторые примечания для добавления здесь: (A) Я решил использовать массивы для представления объектов времени и продолжительности, поскольку они помогают группировать внутренние поля этих понятий (часы, минуты, секунды, нано). Можно также использовать отдельные целые числа. (B) Я полагаюсь на макросы (define-fun ...) очень сильно, и это может сделать ограничения немного сложными, но я не знаю, что еще можно было бы использовать для достижения требуемого уровня выразительности и ясности что текущий код имеет. (C) В настоящее время нет ограничений, ограничивающих поля времени, поэтому значение поля минут, например, может быть 78.Следует добавить утверждения, которые ограничивают секунды до 59, минут до 59 и часов до 23, но я не нашел элегантный способ сделать это.

3. Я предполагаю, что у меня есть разрешимый фрагмент FOL - QF_LIA - поскольку все ограничения объявляются с использованием линейных функций над целыми константами. Тем не менее, я попытался запустить the attached code через Z3 и даже после 40 минут работы локально на среднем компьютере он по-прежнему не возвращается с разрешением (sat/unsat). На самом деле я не знаю, может ли он решить проблему вообще. Возможно, мое предположение о том, что я в QF-LIA ошибается, и также возможно, что Z3 борется с этим типом ограничений. Я могу добавить, что, когда я пробовал более простые ограничения, Z3 удалось достичь разрешения, но я заметил, что созданные ими модели были очень сложными с большим количеством внутренних структур. Может кто-нибудь, пожалуйста, дайте мне некоторые идеи, чтобы исследовать здесь? Онлайн-прокси Z3 с моим кодом можно найти here. Я еще не пробовал других решателей SMT.

4. Я не знаю о параллельных работах, которые пытаются определить временные ограничения этого типа в SMT-LIB. Я действительно ценю ссылки на существующие работы.

Спасибо!

Answer 1

Мне нравится ваш подход, но я думаю, что вы слишком усложняете ситуацию, определяя свои собственные виды, и особенно используя теорию массивов.

Кроме того, математически целые теории сложнее, чем их реальные аналоги. Например, «п = рд, решить для р» является тривиальной, если п, р и д являются вещественные числа, но если они целые числа, то это число факторинг, которое трудно. Аналогично ^{х п} + у ^п = г ^п, п> 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))