Методы автоматизации доказательства NP-полноты двумерных локально зависимых задач Дворкин М. Э. Научный руководитель: Корнеев Г. А., к. т. н., доцент КТ. - презентация

1 Методы автоматизации доказательства NP-полноты двумерных локально зависимых задач Дворкин М. Э. Научный руководитель: Корнеев Г. А., к. т. н., доцент КТ СПбГУ ИТМО

2 Двумерные локально зависимые задачи Вход: поле h×w Вопрос: существует ли заполнение? Корректность заполнения = проверка квадратов s×s Примеры: Головоломки – Сапер – Какуро (CROSS SUM) Замощение данным набором полимино – (p,q)-замощение 2Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

3 Применение устройств «На языке задачи L» выражается известная NP-полная задача Используются «устройства» (gadgets) и провода, соединяющие их Устройства могут быть сложны 3Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

4 Постановка задачи Автоматизация построения устройств с заданной функциональностью Описание наборов устройств, достаточных для доказательства NP-полноты Программная реализация Применение для доказательства NP-полноты конкретных задач – N-CROSS SUM 4Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

5 Сведение 1-in-3 SAT к L Задача 1-in-3 SAT: Вход: конъюнкция из предикатов R(A, B, C) Вопрос: выполнима ли конъюнкция? Удобна, поскольку истинность конъюнкций проверяется независимо 5Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

6 Одинарные и двойные провода Провод придумывается человеком, зачастую просто Устройство «создание провода» не всегда существует Рассматриваются двойные провода: – «в фазе» – «в противофазе» 6Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

7 Набор устройств для двойных проводов «Создание» «Валидатор» «Одинарный провод» «Перекрещивание» «1 из 3» «2 из 3» 7Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

8 Динамическое программирование по профилю Профиль вертикальный «срез» поля, содержит всю необходимую информацию для дальнейшей обработки поля Прямой профиль Проще для понимания Громоздкий переход, большая таблица переходов Изломанный профиль Их число больше Таблица переходов меньше 8Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

9 Подход «перебор всех полей» Перебрать все поля, O(|A| hw ) Для каждого проверить, является ли оно искомым устройством, O(nhwp|B|) Итого: O(|A| hw nhwp|B|) Улучшение: для разных полей не обрабатывать общие префиксы Время работы: O(|A| hw np|B|) 9Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

10 Метадинамическое программирование Рассмотрим два поля после обработки первых i клеток. Что если все совпадает? Метапрофиль множества достижимых профилей для каждого набора булевых значений входных проводов После обработки i-й клетки все поля с одинаковыми мета профилями можно отождествить 10Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

11 Метадинамическое программирование O(min(|A| hw np|B|, |A||B|nphw2 np )) Критична высота рассматриваемого поля Если после обработки столбца то же множество мета профилей, что и до нее, можно остановиться Для каждого мета профиля хранится одно поле-представитель (самое «красивое») 11Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

12 Задача (2,3)-замощения 12Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

13 Задача 4-CROSS SUM (открытый вопрос) 13Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

14 Задача 4-CROSS SUM (открытый вопрос) 14Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.

15 Спасибо за внимание Есть ли вопросы? 15Автоматизация доказательства NP-полноты двумерных задач Дворкин М. Э.