Програмування з обмеженнями

Галузь знань: 12 Інформаційні технології
Спеціальність: 121 Інженерія програмного забезпечення
Освітня програма: Програмна інженерія

Викладач: професор Кривий Сергій Лук'янович (лекції)

Викладається: в 8-му семестрі баалаврату.
Загальний обсяг: 38 год, з яких:
  • Лекції – 32 год.
  • Самостійна робота – 6 год.

Мета та завдання дисципліни

Мета та завдання дисципліни – опанування методами розробки інформаційних систем на основі методів програмування з обмеженнями та їх застосування до розробки, аналізу і верифікації алгоритмів та програм.

Предмет дисципліни

Предмет навчальної дисципліни Програмування з обмеженнями включає в себе проблему розв'язання обмежень лінійного типу над неперервними та дискретними областями. До перших відносяться поля дійсних та раціональних чисел, а до других – відносяться множини натуральних, цілих чисел та скінченні поля і кільця за модулем простого і складеного модуля. Обмеження лінійного типу широко використовуються в процесі аналізу властивостей мереж Петрі, криптографії, обробки сигналів (кодів) розпізнавання образів тощо.

В результаті вивчення навчальної дисципліни студент повинен
знати:
  • основні алгебраїчні структури (групи, кільця, поля, гратки, булеві алгебри),
  • властивості відношень, елементи лінійної алгебри, теорії автоматів.
та вміти:
  • оцінювати складність розв'язання проблеми виконуваності обмежень,
  • розв'язувати проблему виконуваності лінійних обмежень,
  • застсовувати до розв'язання задач верифікації, кодування, розпізнавання зображень тощо.

Вимоги до знань та вмінь

Для вивчення курсу Програмування з обмеженнями студент повинен прослухати наступні курси:
  • дискретна математика,
  • алгебра та геометрія,
  • загальна алгебра,
  • алгоритми та складність,
  • теорія алгоритмів та математична логіка
та повинен вміти:
  • виконувати аналіз проблеми, що виникає, побудову моделей відповідних систем,
  • створювати специфікації цих систем та виконувати верифікацію моделей, що виникли в результаті аналізу проблеми
  • розв'язувати задачі перевірки специфікацій на моделях.

Зв'язок з іншими дисциплінами.

Навчальна дисципліна Програмування з обмеженнями є базовою для вивчення таких спеціальних дисциплін як:
  • Елементи категорного аналізу,
  • Алгебро-автоматні методи проектування програмного забезпечення,
  • Теоретичні основи та методи розробки інформаційних систем,
  • Автоматизація пошуку доведень.

Програма курсу

Змістовий модуль 1: Програмування з обмеженнями: лінійні обмеження, методи розв'язання, побудова базису.

Тема 1: Предмет теорії програмування з обмеженнями
  • Різновиди областей обмежень: обмеження поліноміального і лінійного типів.
  • Дискретні та неперервні області.
  • Проблема виконуваності систем обмежень.
Тема 2: Лінінйні обмеження над неперервними областями
  • Системи лінійних обмежень над полями R i D.
  • Метод Жордана-Гауса та TSS-метод для СЛОР, СЛНР і СЛНН.
Тема 3: Лінійні діофантові обмеження та методи їх розв'язання
  • Автоматні методи розв'язання ЛОДР.
  • Однорідні системи лінійних обмежень над N.
  • Методи розв'язання СЛОР над N: метод Гауса, Контежан-Деві, Потьє, Доменжуда.
Тема 4: Мінімальна породжуюча множина розв'язків
  • Мінімальна породжуючи множина розв'язків СЛОР.
  • TSS-метод побудови мінімальної породжуючої множини розв'язків СЛОР.
  • Властивості TSS-метода.
Тема 5: Проблема виконуваності лінійних обмежень типу нерівностей
  • Порівняння методів.
  • Критерій сумісності СЛОР, СЛНДР, СЛОДН.
  • Перевірка сумісності без введення додаткових невідомих.
Тема 6: Лінійні обмеження над множиною {0,1}
  • Методи розв'язання СЛОДР над множиною булевих значень {0,1}.
  • Три алгоритми побудови базису множини розв'язків СЛОДР.
Тема 7: Лінійні обмеження в полі лишків
  • Базис множини розв'язків в полі за модулем простого числа.
  • TSS-метод розв'язання СЛОДР і СЛНР.
  • Алгоритми побудови базису множини розв'язків СЛОДР та їх часові характеристики.
Тема 8: Лінійні обмеження в кільці лишків
  • Базис множини розв'язків в кільці цілих чисел.
  • TSS-метод розв'язання СЛОДР і СЛНР.
  • Алгоритми побудови базису множини розв'язків СЛОДР та їх часові характеристики.
Модульна контрольна робота 1

Змістовий модуль 2: Застосування: штучний інтелект, мережі Петрі, кодування, математичні ігри, розпізнавання зображень.

Тема 9: Затосування лінійних обмежень в арифметиці Пресбургера
  • Застосування лінійних обмежень в арифметиці Пресбургера.
  • Перевірка виконуваності формул арифметики Пресбургера.
  • Алгоритм Комона.
Тема 10: Затосування лінійних обмежень до аналізу властивостей МП I
  • Застосування при аналізі властивостей мереж Петрі.
  • Аналіз структурних властивостей МП.
  • Аналіз обмеженості та живучості МП.
  • Побудова множини пасток і сифонів МП.
Тема 11: Затосування лінійних обмежень до аналізу властивостей МП II
  • Побудова множини інваріантів переходів і місць в МП.
  • Аналіз властивостей МП на основі інваріантів.
Тема 12: Застосування лінійних обмежень в області телекомунікації
  • Дослідження властивостей різних моделей телефонних мереж.
Тема 13: Застосування лінійних обмежень в області штучного інтелекту
  • Застосування лінійних обмежень в області уніфікації при пошуку доведень в численні предикатів першого порядку.
  • Аналіз суперечності множини диз'юнктів.
Тема 14: Застосування лінійних обмежень в області математичних ігор та кодування
  • Застосування в області математичних ігор та кодуванні.
  • Розпізнавання зображень на площині.
  • Підведення підсумків.
Модульна контрольна робота 2

Рекомендована література

Основна:

  1. Кривий С.Л. Дискретна математика: вибрані питання. – Вид. дім «Києво-Могилянська академія». – 2007. – 570 с.
  2. Лекции по дискретной математике. / Капитонова Ю.В., Кривой С.Л., Летичевский А.А., Луцкий Г.М., Санкт-Петербург. – БХВ. – 2005. – 634 стр.
  3. Глушков В.М., Цейтлин Г.Е, Ющенко Е.Л. Алгебра, язики, программирование. К.: Наукова думка, 1989. – 376 с.
  4. Котов В.Е. Сети Петри. – М.: Наука. – 1974. – 201 с.
  5. Кривий С.Л. Лінійні діофантові обмеження та їх застосування. Київ-Чернівці: Букрек. – 2015 р. – 224 с.
  6. Донец Г.А. Решение задачи о сейфе на (0, 1) матрицах. // Кибернетика и сист. анализ. – 2002. – № 1. – С. 98-105.
  7. Донец Г.А. Решение задачи о построении линейной мозаики. Теория оптимальных решений. – К.: Институт кибернетики им. В.М. Глушкова НАН Украины. – 2005. – С. 15-24.
  8. Зикман Й., Сабо Р. Универсальная унификация и классификация эквациональных теорий. – Кибернетический сборник (новая серия). – 1986. – вып. 21. – С. 213-234.
  9. Крывый С.Л., Матвеева Л.Е., Гжывач В. Автоматный метод решения систем линейных ограничений в области {0,1}. – Болгария. – Труды междунар. конф. KDS-2005. – том 2. – 2005. – С. 389-394.
  10. Крывый С.Л. Критерий совместности систем линейных диофантовых уравнений над множеством натуральных чисел. // Доповіді НАН України. – 1999. – № 5. – С. 107-112.
  11. Крывый С.Л. Алгоритмы решения систем линейных диофантовых уравнений в полях вычетов. // Кибернетика и сист. анализ, 2007. – № 2. – С. 15-23.
  12. Крывый С.Л. Алгоритмы решения систем линейных уравнений над кольцом вычетов. // Кибернетика и сист. анализ, 2016. – № 5. – С. 149-160.
  13. Крывый С.Л. Алгоритмы построения базиса множества решений систем линейных диофантовых уравнений в кольце целых чисел. // Кибернетика и сист. анализ, 2009. – № 6. – С. 36-41.
  14. Крывый С.Л. Об алгоритмах решения систем линейных диофантовых констрейнтов в области {0,1}. // Кибернетика и сист. анализ. – 2003. – № 5. – С. 58-69.

Додаткова:

  1. Baader F., Ziekmann J. Unification theory. // In Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford University Press. – 1994. – pp. 1-85.
  2. Bockmair A., Weispfenning V. Solving Numerical Constraints. // In Handbook of Automated Reasoning. Elsevier Science Publishers B.V. – 2001. – pp. 753-842.
  3. Clausen M., Fortenbacher A. Efficient solution of linear diophantine equations. / J. Symbolic Computation. – 1989. – Vol. 8. – No. 1,2. – pp. 201-216.
  4. Cohen D., Jeavons P. The Complexity of Constraint Languages. // In Handbook of Constraint Programming. Elsevier. – 2006. – Chap. 8. – pp. 245-280.
  5. Comon H. Constraint solving on terms: Automata techniques (Preliminary lecture notes). // Intern. Summer School on Constraints in Computational Logics: Gif-sur-Yvette, France, September 5-8. – 1999. – 22 p.
  6. Contenjean E., Devie H. An efficient algorithm for solving systems of diophantine equations. // Inform. Comput. – 1994. – No. 113. – Vol. 1. – pp. 143-172.
  7. Contejean E., Ajili F. Avoiding slack variables in the solving of linear diophantine equations and inequations. // TCS. – 1997. – Vol. 173. – pp. 183-208.
  8. Creignou N., Khanna S., Sudan M. Complexity Classification of Boolean Constraint Satisfaction Problems. // SIAM Monographs on Discrete Mathematics and Applications: Society for Industrial and Applied Mathematics. Philadelphia. PA. – 2001. – Vol. 7. – 347 p.
  9. Domenjoud E. Outils pour la deduction automatique dans les theories associatives-commutatives. // Thesis de Doctorat d'Universite: Universite de Nancy I. – 1991.
  10. Filgueiras M.,Tomas A.P. A Fast Method for Finding the Basis of Non-negative Solutions to a Linear Diophantine Equation. // J. Symbolic Computation. – 1995. – Vol. 19. – No. 2. – pp. 507-526.
  11. Hermann M., Juban L., Kolaitis P.G. On the Complexity of Counting the Hilbert Basis of a Linear Diophantine System. // Springer Verlag. – LNCS. – 1999. – No. 1705. – pp. 13-32.