Дипломная работа по программированию в ограничениях

Обзор

Ещё студентом факультета информатики я взялся за практический вопрос: когда симулятор накапливает множество возможных условий, как заставить его перестать перебирать те, которые уже не могут случиться? Я разработал и оценил для HydLa метод, который опирается на направление изменения величины, чтобы убирать из поиска условия, потерявшие смысл. На эталонной модели общее время симуляции сократилось примерно вдвое.

Эта работа — один из первых фундаментов моей философии дизайна. Программирование в ограничениях научило меня тому, что сложный результат не всегда нужно задавать напрямую: он может вырасти из тщательно определённого пространства правил, приоритетов и границ. Этот способ мышления и лежит сегодня в основе того, как я проектирую через ограничения в эпоху ИИ, — проектирую условия, внутри которых порождающая система вольна действовать.

Аннотация

HydLa — язык моделирования гибридных систем, то есть систем, где непрерывное изменение взаимодействует с дискретными событиями. Устройство языка на основе ограничений позволяет описывать такие системы кратко и симулировать их с высокой точностью. Плата за это в том, что в большой модели симулятор может продолжать проверять огромное число условных правил даже после того, как часть из них потеряла всякое отношение к делу.

В исследовании предложено сокращать эти охраняемые ограничения на ходу. Распознав монотонное поведение — величину, которая продолжает двигаться в одну сторону, — симулятор может установить, что некоторые охранные условия уже никогда не станут истинными, и безопасно прекратить их проверку. Подход оказался особенно действенным на модели с большим числом однотипно охраняемых объектов: измеренное время работы упало примерно до половины исходного.

1. Введение

Гибридная система соединяет непрерывное поведение с дискретными событиями. Прыгающий мяч — простой пример: пока он в воздухе, его положение и скорость меняются непрерывно, но момент удара о поверхность создаёт дискретное событие, меняющее направление. Термостаты, автомобили и роботы содержат внутри ту же смесь, только с более серьёзными последствиями.

HydLa позволяет описывать такие системы математическими и логическими ограничениями, а не выписывать единственную процедурную последовательность. Его симулятор HyLaGI умеет вести символьные вычисления без ошибок округления и работать с неопределёнными параметрами. Однако эта выразительность создаёт проблему масштаба: если модель содержит множество правил, включающихся лишь при определённых условиях, симулятору приходится снова и снова спрашивать про каждое условие, не окажется ли оно следующим.

2. Охраняемые ограничения в симуляции

Охраняемое ограничение — это правило, которое становится активным лишь при выполнении его охранного условия. В эталонной модели выше у каждого участка поверхности своё правило: если мяч достигает нулевой высоты, а его горизонтальное положение лежит внутри этого участка, применяется правило отскока. Значит, чем мельче разделена поверхность, тем больше охранных условий симулятору приходится осматривать.

В эксперименте число участков менялось от 10 до 200. Исходный симулятор замедлялся примерно как квадрат этого числа. Это важно и за пределами игрушечного примера: более крупная модель может представлять множество физических объектов, областей контакта или возможных событий именно в такой охраняемой форме.

3. Где узкое место

Профилирование показало, что замедление распределено по симулятору неравномерно. При 100 участках поверхности 96 % измеренного времени работы уходило в FindMinTime — операцию, которая ищет ближайшее возможное следующее событие. Она снова и снова вычисляла охранные условия всех ограничений-кандидатов.

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

4. Сокращение охраняемых ограничений

Представьте мяч, который скачет вниз по лестнице. Как только мяч миновал ступень и продолжает двигаться вперёд, эта ступень больше не может на него повлиять. Человек, глядя на рисунок, сразу отбрасывает ступени позади мяча; исходный алгоритм продолжал проверять каждую из них.

Трудность в том, чтобы доказать: отброшенное охранное условие не понадобится позже. Убрать его только потому, что сейчас оно ложно, значит рискнуть молча получить неверный результат, если оно снова станет истинным. Поэтому предложение опирается на монотонность — на то, гарантированно ли переменная продолжает возрастать или продолжает убывать на некотором интервале времени.

4.1 Подход для равномерной монотонности

Первый подход применим, когда переменная движется в одну сторону на протяжении всей симуляции. В модели с разделённой поверхностью горизонтальное положение мяча всегда возрастает. Стоит ему уйти за пределы участка, и условие этого участка уже никогда не выполнится. Методы верификации моделей позволяют установить это свойство до симуляции, а значит, устаревшие охранные условия можно безопасно убирать по ходу выполнения.

4.2 Подход для перемежающейся монотонности

Многие реальные системы не движутся в одну сторону вечно. Переменная может возрастать, развернуться, а затем убывать. Поэтому в статье намечен второй подход: начать с предполагаемого направления, следить за этим предположением с помощью утверждений и перезапускать логику сокращения с той точки, где направление меняется. Охранные условия, убранные для одного монотонного интервала, восстанавливаются с началом следующего.

5. Результаты экспериментов

Я реализовал подход равномерной монотонности и оценил его на модели с разделённой поверхностью. И исходный, и предложенный алгоритм всё равно работали дольше по мере роста числа участков, но предложенный вариант неизменно выполнял меньше работы. При сравнении подогнанных кривых старший коэффициент упал с 1,1463 до 0,6083; для этой эталонной задачи общее время симуляции сократилось примерно вдвое.

Это не утверждение, что любая модель на HydLa станет вдвое быстрее. Результат показывает, где метод помогает: в моделях с множеством охраняемых объектов и доказуемым направлением изменения, где охранные условия по ходу выполнения становятся навсегда несущественными.

6. Заключение и дальнейшая работа

Исследование показало, что эффективность симуляции повышает не только более быстрое низкоуровневое вычисление, но и знание о самой модели. Используя монотонность, чтобы распознать, какие возможности стали невозможными, HyLaGI может сжимать набор активных ограничений, не меняя результат.

Реализованный эксперимент охватил равномерную монотонность. Статья оставила два направления на будущее: оценить метод на основе утверждений для перемежающегося поведения и использовать другие инварианты, помимо монотонности, чтобы находить новые ограничения, которые можно безопасно убрать.