Что: | Лекция |
Когда: | Вторник, 14 апреля 2009, 16:20–17:50 |
Где: | ПОМИ РАН |
Доказательство NP–полноты некоторой задачи L в большинстве случаев представляет собой сведение какой–нибудь известной NP–полной задачи к задаче L. Например, можно «выразить на языке задачи L» провода, передающие логические значения, и логические элементы. Тогда задача SAT сводится к L. Именно так доказывают NP–полноту задач на клетчатом поле («Сапер», «Какуро», замощение тримино и др.) При этом во всех известных работах соответствующие элементы (логические операции, скрещивание проводов) создаются вручную, и это нетривиальная творческая задача. Предлагаемый подход — автоматическое построение этих элементов. Для этого используется модифицированное динамическое программирование по профилю: метадинамическое программирование. Предлагаемый подход позволяет автоматизировать процесс доказательства NP–полноты задач на клетчатом поле. В частности, была доказана NP–полнота задачи 4–CROSS SUM, что ранее являлось открытым вопросом.