City: Test Saint Petersburg Novosibirsk Kazan Language: Русский English

Автоматизация доказательства NP–полноты некоторых двумерных задач (Михаил Дворкин)
Seminar on Computer Science

What: Lecture
When: Tuesday, 14 April 2009, 16:20–17:50
Where: ПОМИ РАН

Description

Доказательство NP–полноты некоторой задачи L в большинстве случаев представляет собой сведение какой–нибудь известной NP–полной задачи к задаче L. Например, можно «выразить на языке задачи L» провода, передающие логические значения, и логические элементы. Тогда задача SAT сводится к L. Именно так доказывают NP–полноту задач на клетчатом поле («Сапер», «Какуро», замощение тримино и др.) При этом во всех известных работах соответствующие элементы (логические операции, скрещивание проводов) создаются вручную, и это нетривиальная творческая задача. Предлагаемый подход — автоматическое построение этих элементов. Для этого используется модифицированное динамическое программирование по профилю: метадинамическое программирование. Предлагаемый подход позволяет автоматизировать процесс доказательства NP–полноты задач на клетчатом поле. В частности, была доказана NP–полнота задачи 4–CROSS SUM, что ранее являлось открытым вопросом.