Представление временных ограничений в 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)
)

Остальные определения можно найти в этом файле.

Исходя из этого, я могу выразить ограничения с помощью ряда утверждений:

(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 с моим кодом можно найти здесь. Я еще не пробовал другие решения для SMT.

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

Спасибо!

Answer 1

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

Кроме того, математически, целочисленные теории сложнее, чем их реальные аналоги. Например, "n = pq, решить для p" тривиально, если 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))