HORN-SAT (летняя практика) — различия между версиями
Eperzhand (обсуждение | вклад) |
Eperzhand (обсуждение | вклад) |
||
(не показана одна промежуточная версия ещё одного участника) | |||
Строка 3: | Строка 3: | ||
|mentor=Дворянский Леонид Владимирович | |mentor=Дворянский Леонид Владимирович | ||
|mentor_login={{URLENCODE:Eperzhand|WIKI}} | |mentor_login={{URLENCODE:Eperzhand|WIKI}} | ||
− | |organization= | + | |organization=Лаборатория ПОИС |
|hse_profile=www.hse.ru/staff/leo | |hse_profile=www.hse.ru/staff/leo | ||
|email=leo@mathtech.ru | |email=leo@mathtech.ru | ||
− | |thesis= | + | |thesis=yes |
|year=2015 | |year=2015 | ||
|categorize=yes | |categorize=yes |
Текущая версия на 22:54, 1 июня 2015
Автор | Дворянский Леонид Владимирович [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