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

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

Версия 00:50, 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