Presburger Functional Synthesis: Complexity and Tractable Normal Forms

## Контекст Проблема функциональной синтеза заключается в автоматическом синтезе функции, удовлетворяющей заданному отношению между входными и выходными параметрами, заданным логическим формулой. Эта задача находит применение в программной инженерии, автоматической программной инженерии и логическом программировании. Одна из важных областей применения — функциональная синтезирование в теории Пресбургеровской арифметики (Presburger Arithmetic). Она дифференцируется тем, что работает с подсчётными свойствами, включая добавление и удаление чисел, что усложняет синтез. Несмотря на развитие методов функциональной синтеза для булевых и первого порядка логических теорий, к теории Пресбургера этот вопрос пока до конца не был рассмотрен. Мотивация заключается в изучении возможности и сложности использования теории Пресбургера в синтезе функций. ## Метод Мы предлагаем алгоритм для решения функциональной синтеза в теории Пресбургера (Presburger Functional Synthesis, PFnS). Этот алгоритм основывается на переходе к специальной нормальной форме, PSyNF (Presburger Syntactic Normal Form). Мы показываем, что PFnS может быть решено за экспоненциальное время, с соответствующей нижней теоретической оценкой. Алгоритм состоит в переводе спецификации в PSyNF, после чего синтезируется функция. Для доказательства того, что PSyNF может быть эффективно проверено и решено, мы используем техники логического анализа и оптимизации. Мы также рассматриваем ситуации, когда PSyNF может быть эффективно преобразован в другие нормальные формы, сохраняя эффективность. ## Результаты Мы проводим эксперименты, сравнивая PFnS с булевой функциональной синтезой (BFnS). Наши результаты показывают, что PFnS является экспоненциально сложной, но полиномиально решаемой в определённых нормальных формах. Мы проверяем экспериментально преобразования спецификаций в PSyNF и проверяем полученные результаты. Также мы сравниваем сложность PFnS с BFnS и показываем, что последняя требует больших ресурсов для решения, что демонстрирует разницу в сложности для разных логических теорий. ## Значимость Областьми применения PFnS являются автоматическое программирование, логические вычисления и синтез сложных функций в теории Presburger. Наш алгоритм позволяет эффективно решать задачи синтеза в этой теории, что может использоваться в проектировании алгоритмов, автоматическом доказательстве свойств программ и анализе сложных логических систем. Значимость заключается в том, что мы предлагаем новый подход к решению задач синтеза, который может быть обобщён и применён к дру