HORN-SAT (летняя практика)

Автор	Дворянский Леонид Владимирович [www.hse.ru/staff/leo Профиль на сайте ВШЭ] Электронная почта
Организация	Лаборатория ПОИС
Учебный год	2015
По теме задания можно сделать курсовую в следующем году обучения

Задание

Формулы Хорна играют важную роль в компьютерных науках. С помощью формул Хорна можно решать различные задачи из прикладной теории графов, логического программирования, сетей Петри. Однако, после того, как мы закодировали задачу в виде формулы Хорна, нужно найти при каких значениях переменных [math]x_1...x_n[/math] такая формула будет истинна.

Вашей задачей будет:

• разобраться с понятием формул Хорна;
• реализовать формулы Хорна в виде структуры данных на компьютере;
• разобраться и реализовать алгоритм/алгоритмы HORN-SAT;

Какие начальные требования?

• C/С++/Java (при большом желании и аргументации можно другой язык, но только после прочтения: http://maryrosecook.com/blog/post/the-fibonacci-heap-ruins-my-life)
• Основы дискретной математики и мат. логики (см. ссылку: neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ)

Какие будут использоваться технологии?

Никаких дополнительных технологий не предполагается.

При желании можно:

• ускорять нахождение решения HORN-SAT (или любой другой проблемы) оптимизируя код на низком уровне (ассемблер, CUDA);
• масштабировать программу с помощью облачных вычислений;
• реализовывать/придумывать/испытывать более эффективные алгоритмы для специальных подклассов.

Какая дополнительная литература понадобится?

Вводные статьи:

Algorithms for the Satisfiability (SAT) Problem: A Survey J. Gu, P. W. Purdom, J. Franco, and B. W. Wah, in "Satisfiability Problem: Theory and Applications", DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997, pp. 19-152.

Dowling, W., and Gallier, J., (1984) "Linear-time algorithms for testing the satisfiability of propositional Horn formulae". Journal of Logic Programming, 3, 267-284