HORN-SAT (летняя практика) — различия между версиями

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
 
Строка 6: Строка 6:
 
|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