https://wikicshse.ru/index.php?action=history&feed=atom&title=HORN-SAT_%28%D0%BB%D0%B5%D1%82%D0%BD%D1%8F%D1%8F_%D0%BF%D1%80%D0%B0%D0%BA%D1%82%D0%B8%D0%BA%D0%B0%29 2026-06-06T15:46:28Z История изменений этой страницы в вики MediaWiki 1.45.3 https://wikicshse.ru/index.php?title=HORN-SAT_(%D0%BB%D0%B5%D1%82%D0%BD%D1%8F%D1%8F_%D0%BF%D1%80%D0%B0%D0%BA%D1%82%D0%B8%D0%BA%D0%B0)&diff=326&oldid=prev 2015-06-01T19:54:57Z

<p>Migrated current public revision from wiki.cs.hse.ru</p> <p><b>Новая страница</b></p><div>{{Карточка_задания_на_летнюю_практику<br /> |name=HORN-SAT<br /> |mentor=Дворянский Леонид Владимирович<br /> |mentor_login={{URLENCODE:Eperzhand|WIKI}}<br /> |organization=Лаборатория ПОИС<br /> |hse_profile=www.hse.ru/staff/leo<br /> |email=leo@mathtech.ru<br /> |thesis=yes<br /> |year=2015<br /> |categorize=yes<br /> }}<br /> <br /> === Задание ===<br /> Формулы Хорна играют важную роль в компьютерных науках.<br /> С помощью формул Хорна можно решать различные задачи из прикладной теории графов, логического программирования, сетей Петри.<br /> Однако, после того, как мы закодировали задачу в виде формулы Хорна, нужно найти при каких значениях переменных [math]x_1...x_n[/math] такая формула будет истинна. <br /> <br /> Вашей задачей будет:<br /> * разобраться с понятием формул Хорна;<br /> * реализовать формулы Хорна в виде структуры данных на компьютере;<br /> * разобраться и реализовать алгоритм/алгоритмы HORN-SAT;<br /> <br /> === Какие начальные требования? ===<br /> * C/С++/Java (при большом желании и аргументации можно другой язык, но только после прочтения: http://maryrosecook.com/blog/post/the-fibonacci-heap-ruins-my-life)<br /> * Основы дискретной математики и мат. логики (см. ссылку: neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ)<br /> <br /> === Какие будут использоваться технологии? ===<br /> Никаких дополнительных технологий не предполагается.<br /> <br /> При желании можно:<br /> * ускорять нахождение решения HORN-SAT (или любой другой проблемы) оптимизируя код на низком уровне (ассемблер, CUDA);<br /> * масштабировать программу с помощью облачных вычислений;<br /> * реализовывать/придумывать/испытывать более эффективные алгоритмы для специальных подклассов.<br /> <br /> === Какая дополнительная литература понадобится? ===<br /> Вводные статьи:<br /> <br /> Algorithms for the Satisfiability (SAT) Problem: A Survey <br /> J. Gu, P. W. Purdom, J. Franco, and B. W. Wah, in &quot;Satisfiability Problem: Theory and Applications&quot;, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997, pp. 19-152.<br /> <br /> Dowling, W., and Gallier, J., (1984) &quot;Linear-time algorithms for testing the satisfiability of propositional Horn formulae&quot;. Journal of Logic Programming, 3, 267-284</div>

imported>Eperzhand