Контекст
Чтобы узнать больше о решении и оптимизации SMT, я пытаюсь решить конкретную проблему, используя Z3 . Я успешно смоделировал проблему (она компилируется и запускается), но я думаю, что, возможно, я делаю что-то не так, потому что требуются секунды, чтобы решить даже в небольших случаях, и минуты в реалистичных сценариях. Я чувствую, что, должно быть, что-то упустил.
Мои вопросы:
- Это нормально, что эта проблема занимает так много времени, чтобы решить? У меня нет предыдущего опыта, так что, может быть, так оно и есть.
- Является ли Z3 подходящим инструментом для работы? Если нет, то что бы вы порекомендовали мне попробовать?
Описание задачи оптимизации
Представьте, что вы организуете кулинарную мастерскую. Есть i учителей, j студентов и k практических заданий. Для каждого практического задания учеников нужно разделить на i групп, чтобы они могли работать над заданием под присмотром учителя. Есть два дополнительных требования:
- Каждый учитель должен учить каждого ученика хотя бы один раз
- Мы хотим максимизировать количество студентов, которые знакомятся друг с другом во время выполнения заданий (то есть количество пар студентов, которые работали вместе хотя бы в одном задании)
Например, с 2 преподавателями, 6 студентами и 2 лабораторными заданиями вы можете получить следующее подразделение:
Задание 1:
- Учитель 1: ученик 1, ученик 2, ученик 3
- Учитель 2: ученик 4, ученик 5, ученик 6
Задание 2:
- Учитель 1: ученик 4, ученик 5, ученик 6
- Учитель 2: ученик 1, ученик 2, ученик 3
Здесь каждый учитель учил каждого ученика. Однако по необходимости это означает, что количество студентов, которые познакомились друг с другом, невелико. Фактически, группы не менялись между заданиями 1 и 2, только учителя.
Объяснение проблемы с Z3
Я написал программу для генерации набора операторов SMT-LIB, которые затем подаются в Z3. Для предыдущего примера с 6 студентами, 2 учителями и 2 заданиями мы получаем следующий код (вы также можете проверить его здесь , если хотите):
Определить вспомогательную функцию для преобразования логических значений в целые числа:
(define-fun bool2int ((x Bool)) Int (ite x 1 0))
Объявите константы в форме s{x}_a{y}_t{z}, которые указывают, выполняет ли ученик x задание y с учителем z:
(declare-const s1_a1_t1 Bool)
(declare-const s1_a1_t2 Bool)
(declare-const s1_a2_t1 Bool)
(declare-const s1_a2_t2 Bool)
(declare-const s2_a1_t1 Bool)
(declare-const s2_a1_t2 Bool)
(declare-const s2_a2_t1 Bool)
(declare-const s2_a2_t2 Bool)
(declare-const s3_a1_t1 Bool)
(declare-const s3_a1_t2 Bool)
(declare-const s3_a2_t1 Bool)
(declare-const s3_a2_t2 Bool)
(declare-const s4_a1_t1 Bool)
(declare-const s4_a1_t2 Bool)
(declare-const s4_a2_t1 Bool)
(declare-const s4_a2_t2 Bool)
(declare-const s5_a1_t1 Bool)
(declare-const s5_a1_t2 Bool)
(declare-const s5_a2_t1 Bool)
(declare-const s5_a2_t2 Bool)
(declare-const s6_a1_t1 Bool)
(declare-const s6_a1_t2 Bool)
(declare-const s6_a2_t1 Bool)
(declare-const s6_a2_t2 Bool)
Объявите ограничения, чтобы гарантировать, что для каждого задания студент должен работать под наблюдением ровно одного учителя:
(assert (= 1 (+ (bool2int s1_a1_t1) (bool2int s1_a1_t2) )))
(assert (= 1 (+ (bool2int s1_a2_t1) (bool2int s1_a2_t2) )))
(assert (= 1 (+ (bool2int s2_a1_t1) (bool2int s2_a1_t2) )))
(assert (= 1 (+ (bool2int s2_a2_t1) (bool2int s2_a2_t2) )))
(assert (= 1 (+ (bool2int s3_a1_t1) (bool2int s3_a1_t2) )))
(assert (= 1 (+ (bool2int s3_a2_t1) (bool2int s3_a2_t2) )))
(assert (= 1 (+ (bool2int s4_a1_t1) (bool2int s4_a1_t2) )))
(assert (= 1 (+ (bool2int s4_a2_t1) (bool2int s4_a2_t2) )))
(assert (= 1 (+ (bool2int s5_a1_t1) (bool2int s5_a1_t2) )))
(assert (= 1 (+ (bool2int s5_a2_t1) (bool2int s5_a2_t2) )))
(assert (= 1 (+ (bool2int s6_a1_t1) (bool2int s6_a1_t2) )))
(assert (= 1 (+ (bool2int s6_a2_t1) (bool2int s6_a2_t2) )))
Объявите ограничения, чтобы каждый учитель обучал каждого ученика хотя бы один раз:
(assert (or s1_a1_t1 s1_a2_t1 ))
(assert (or s2_a1_t1 s2_a2_t1 ))
(assert (or s3_a1_t1 s3_a2_t1 ))
(assert (or s4_a1_t1 s4_a2_t1 ))
(assert (or s5_a1_t1 s5_a2_t1 ))
(assert (or s6_a1_t1 s6_a2_t1 ))
(assert (or s1_a1_t2 s1_a2_t2 ))
(assert (or s2_a1_t2 s2_a2_t2 ))
(assert (or s3_a1_t2 s3_a2_t2 ))
(assert (or s4_a1_t2 s4_a2_t2 ))
(assert (or s5_a1_t2 s5_a2_t2 ))
(assert (or s6_a1_t2 s6_a2_t2 ))
Объявите ограничения, чтобы гарантировать, что для каждого задания учитель должен обучать ровно 3 ученика. Мы используем >= в сочетании с <=, потому что в некоторых случаях проблемы допускают минимальное и максимальное количество студентов (т.е. когда j % i != 0).
(define-fun t1_a1 () Int (+ (bool2int s1_a1_t1) (bool2int s2_a1_t1) (bool2int s3_a1_t1) (bool2int s4_a1_t1) (bool2int s5_a1_t1) (bool2int s6_a1_t1) ))
(assert (>= 3 t1_a1))
(assert (<= 3 t1_a1))
(define-fun t1_a2 () Int (+ (bool2int s1_a2_t1) (bool2int s2_a2_t1) (bool2int s3_a2_t1) (bool2int s4_a2_t1) (bool2int s5_a2_t1) (bool2int s6_a2_t1) ))
(assert (>= 3 t1_a2))
(assert (<= 3 t1_a2))
(define-fun t2_a1 () Int (+ (bool2int s1_a1_t2) (bool2int s2_a1_t2) (bool2int s3_a1_t2) (bool2int s4_a1_t2) (bool2int s5_a1_t2) (bool2int s6_a1_t2) ))
(assert (>= 3 t2_a1))
(assert (<= 3 t2_a1))
(define-fun t2_a2 () Int (+ (bool2int s1_a2_t2) (bool2int s2_a2_t2) (bool2int s3_a2_t2) (bool2int s4_a2_t2) (bool2int s5_a2_t2) (bool2int s6_a2_t2) ))
(assert (>= 3 t2_a2))
(assert (<= 3 t2_a2))
Объявите функции, чтобы отслеживать, какие студенты работали вместе для выполнения задания:
(define-fun s1_has_met_s2 () Bool (or (and s1_a1_t1 s2_a1_t1) (and s1_a2_t1 s2_a2_t1) (and s1_a1_t2 s2_a1_t2) (and s1_a2_t2 s2_a2_t2) ))
(define-fun s1_has_met_s3 () Bool (or (and s1_a1_t1 s3_a1_t1) (and s1_a2_t1 s3_a2_t1) (and s1_a1_t2 s3_a1_t2) (and s1_a2_t2 s3_a2_t2) ))
(define-fun s1_has_met_s4 () Bool (or (and s1_a1_t1 s4_a1_t1) (and s1_a2_t1 s4_a2_t1) (and s1_a1_t2 s4_a1_t2) (and s1_a2_t2 s4_a2_t2) ))
(define-fun s1_has_met_s5 () Bool (or (and s1_a1_t1 s5_a1_t1) (and s1_a2_t1 s5_a2_t1) (and s1_a1_t2 s5_a1_t2) (and s1_a2_t2 s5_a2_t2) ))
(define-fun s1_has_met_s6 () Bool (or (and s1_a1_t1 s6_a1_t1) (and s1_a2_t1 s6_a2_t1) (and s1_a1_t2 s6_a1_t2) (and s1_a2_t2 s6_a2_t2) ))
(define-fun s2_has_met_s3 () Bool (or (and s2_a1_t1 s3_a1_t1) (and s2_a2_t1 s3_a2_t1) (and s2_a1_t2 s3_a1_t2) (and s2_a2_t2 s3_a2_t2) ))
(define-fun s2_has_met_s4 () Bool (or (and s2_a1_t1 s4_a1_t1) (and s2_a2_t1 s4_a2_t1) (and s2_a1_t2 s4_a1_t2) (and s2_a2_t2 s4_a2_t2) ))
(define-fun s2_has_met_s5 () Bool (or (and s2_a1_t1 s5_a1_t1) (and s2_a2_t1 s5_a2_t1) (and s2_a1_t2 s5_a1_t2) (and s2_a2_t2 s5_a2_t2) ))
(define-fun s2_has_met_s6 () Bool (or (and s2_a1_t1 s6_a1_t1) (and s2_a2_t1 s6_a2_t1) (and s2_a1_t2 s6_a1_t2) (and s2_a2_t2 s6_a2_t2) ))
(define-fun s3_has_met_s4 () Bool (or (and s3_a1_t1 s4_a1_t1) (and s3_a2_t1 s4_a2_t1) (and s3_a1_t2 s4_a1_t2) (and s3_a2_t2 s4_a2_t2) ))
(define-fun s3_has_met_s5 () Bool (or (and s3_a1_t1 s5_a1_t1) (and s3_a2_t1 s5_a2_t1) (and s3_a1_t2 s5_a1_t2) (and s3_a2_t2 s5_a2_t2) ))
(define-fun s3_has_met_s6 () Bool (or (and s3_a1_t1 s6_a1_t1) (and s3_a2_t1 s6_a2_t1) (and s3_a1_t2 s6_a1_t2) (and s3_a2_t2 s6_a2_t2) ))
(define-fun s4_has_met_s5 () Bool (or (and s4_a1_t1 s5_a1_t1) (and s4_a2_t1 s5_a2_t1) (and s4_a1_t2 s5_a1_t2) (and s4_a2_t2 s5_a2_t2) ))
(define-fun s4_has_met_s6 () Bool (or (and s4_a1_t1 s6_a1_t1) (and s4_a2_t1 s6_a2_t1) (and s4_a1_t2 s6_a1_t2) (and s4_a2_t2 s6_a2_t2) ))
(define-fun s5_has_met_s6 () Bool (or (and s5_a1_t1 s6_a1_t1) (and s5_a2_t1 s6_a2_t1) (and s5_a1_t2 s6_a1_t2) (and s5_a2_t2 s6_a2_t2) ))
Максимальное количество людей, которые встретились:
(maximize (+ (bool2int s1_has_met_s2)(bool2int s1_has_met_s3)(bool2int s1_has_met_s4)(bool2int s1_has_met_s5)(bool2int s1_has_met_s6)(bool2int s2_has_met_s3)(bool2int s2_has_met_s4)(bool2int s2_has_met_s5)(bool2int s2_has_met_s6)(bool2int s3_has_met_s4)(bool2int s3_has_met_s5)(bool2int s3_has_met_s6)(bool2int s4_has_met_s5)(bool2int s4_has_met_s6)(bool2int s5_has_met_s6)))
Ограничения
Основное ограничение, с которым я сталкиваюсь, - это время, необходимое для запуска моделей. Это просто не масштабируется:
- 6 учеников, 2 учителя, 2 задания: 100 мс
- 7 учеников, 3 учителя, 3 задания: 10 с
- 9 учеников, 3 учителя, 3 задания: убиты через минуту (кто знает, сколько времени это займет ...)
Моя цель - запустить это примерно с 20 студентами, 3 преподавателями и 5 заданиями ... Однако, с текущей настройкой, я сомневаюсь, что Z3 когда-нибудь завершит вычисление этого.
Эта суть содержит код SMT-LIB для экземпляра с 9 учениками, 3 учителями и 3 заданиями.В некоторой степени меня не удивляет то, что это занимает так много времени ... Функция, которую я хочу максимизировать, действительно увеличилась в размерах.
Заключительные замечания
Как вы можете видеть, Я застрял.Насколько я знаю, не существует более простого способа выражения ограничений и целевой функции для этой задачи.Мне кажется, что я достиг фундаментального ограничения.Итак, здесь снова мои вопросы:
- Это нормально, что эта проблема занимает так много времени, чтобы решить?У меня нет предыдущего опыта, так что, может быть, так оно и есть.
- Является ли Z3 подходящим инструментом для работы?Если нет, то что бы вы порекомендовали мне попробовать?