HORN-SAT (летняя практика) - История изменений

Eperzhand в 19:54, 1 июня 2015

2015-06-01T19:54:57Z

← Предыдущая версия		Версия от 19:54, 1 июня 2015
Строка 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

Katya в 14:15, 1 июня 2015

2015-06-01T14:15:10Z

← Предыдущая версия		Версия от 14:15, 1 июня 2015
Строка 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

Eperzhand в 21:50, 31 мая 2015

2015-05-31T21:50:48Z

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

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

Eperzhand: New page using form Новое_задание_на_летнюю_практику

2015-05-31T21:48:00Z

New page using form Новое_задание_на_летнюю_практику

Новая страница

{{Карточка_задания_на_летнюю_практику
|name=HORN-SAT
|mentor=Дворянский Леонид Владимирович
|mentor_login={{URLENCODE:Eperzhand|WIKI}}
|organization=НИУ ВШЭ
|hse_profile=www.hse.ru/staff/leo
|email=leo@mathtech.ru
|thesis=
|year=2015
|categorize=yes
}}

=== Задание ===
Формулы Хорна играют важную роль в компьютерных науках.
С помощью формул Хорна можно решать различные задачи из прикладной теории графов, логического программирования, сетей Петри.
Однако после того, как мы закодировали задачу в виде формулы Хорна, для ее решения нужно найти при каких значениях переменных [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