Сложность решения задачи выполнимости булевых формул алгоритмами, основанными на расщеплении тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Соколов, Дмитрий Олегович АВТОР
кандидата физико-математических наук УЧЕНАЯ СТЕПЕНЬ
Санкт-Петербург МЕСТО ЗАЩИТЫ
2014 ГОД ЗАЩИТЫ
   
01.01.06 КОД ВАК РФ
Автореферат по математике на тему «Сложность решения задачи выполнимости булевых формул алгоритмами, основанными на расщеплении»
 
Автореферат диссертации на тему "Сложность решения задачи выполнимости булевых формул алгоритмами, основанными на расщеплении"

На правах рукописи

Соколов Дмитрий Олегович

Сложность решения задачи выполнимости булевых формул алгоритмами, основанными на расщеплении

01.01.06 — математическая логика, алгебра и теория чисел 01.01.09 — дискретная математика и математическая кибернетика

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

и О 2015

Санкт-Петербург — 2014

005559042

005559042

Работа выполнена в лаборатории математической логики ФГБУН Санкт-Петербургского отделения Математического института им. В. А. Стеклова Российской академии наук.

Научные руководители: Гирш Эдуард Алексеевич

доктор физико-математических наук, доцент, ведущий научный сотрудник лаборатории математической логики ФГБУН Санкт-Петербургского отделения Математического института им. В. А. Стеклова Российской академии наук Ицыксон Дмитрий Михайлович

кандидат физико-математических наук, старший научный сотрудник лаборатории математической логики ФГБУН Санкт-Петербургского отделения Математического института ил!. В. А. Стеклова Российской академии наук

Официальные оппоненты: Райгородский Андрей Михайлович

доктор физико-математических наук

профессор ФГОУ ВПО "Московский Государственный Университет им. М.В. Ломоносова" Шень Александр Ханьевич кандидат физико-математических наук

старший научный сотрудник лаборатории № 1 им. М.С. Пинскера ФГБУН Института проблем передачи информации им. A.A. Харкевича Российской академии наук Ведущая организация: ФГАОУВПО "Казанский (Приволжский) федеральный университет"

Защита состоится «4» марта 2015 г. в 17:00 на заседании диссертационного совета Д002.202.02 в ФГБУН Санкт-Петербургском отделении Математического института им. В. А. Стеклова Российской академии наук по адресу: 191023, Санкт-Петербург, наб. р. Фонтанки, 27, к. 311.

С диссертацией можно ознакомиться в библиотеке и на сайте ФГБУН Санкт-Петербургского отделения Математического института им. В. А. Стеклова Российской академии наук, http://www.pdmi.ras.ru/

Автореферат разослан « Z9 »

2015 г.

Ученый секретарь диссертационного совета, д. ф.-м. н.

А. В. Малютин

Общая характеристика работы

Актуальность темы. Задача выполнимости булевых (пропозициональных) формул (SAT) — это задача нахождения по булевой формуле такой подстановки значений переменным, что при применении данной подстановки формула обращается в тождественную истину. Если такая подстановка существует, то формула называется выполнимой; если же нет, то функция, задаваемая данной формулой, является тождественной ложью, и формула является невыполнимой.

SAT — одна из первых задач, для которых была доказана NP-полнота (теорема Кука-Левина (1973)). Это означает, что любая задача из класса NP, который включает в себя широкий круг естественных задач, возникающих на практике, сводится к задаче выполнимости булевых формул. Таким образом существование эффективного алгоритма для SAT (как и доказательство его отсутствия) эквивалентно одной из центральных задач теории сложности о равенстве между классами Р и NP, и таких алгоритмов в настоящее время не известно.

Несмотря на это, формулы, возникающие на практике, успешно решаются прн помощи SAT-солверов (программ для решения задачи выполнимости). Одним из основных подходов к решению задачи выполнимости пропозициональных формул являются DPLL-алгоритмы (названы в честь авторов: Davis, Putnam, Logemann и Loveland), основанные на методе расщепления. DPLL-алгорнтм — рекурсивный алгоритм, который на вход получаст формулу ф, затем запускает процедуру А, которая выбирает переменную х, после этого алгоритм запускает процедуру В для выбора константы с, затем рекурсивно вызывает себя на формуле Ф[х := с], если был найден выполняющий набор, то выдает его, иначе возвращает результат запуска алгоритма на формуле Ф[ж := 1-е]. Рекурсивные вызовы прекращаются, когда формула становится тривиальной. Таким образом, алгоритм расщепления определяется

правилами упрощения и двумя эвристиками: эвристика А выбирает переменную, а эвристика В выбирает, какое значение переменной будет проверено раньше.

Известны экспоненциальные нижние оценки на время работы ВРЬЬ-алгоритмов на невыполнимых формулах, в частности, такие оценки следуют из оценок на размер резолюционных доказательств. В случае выполнимых формул суперполиномиальные нижние оценки на время работы всех возможных О Р Ь Ь-ал го р и тм ы повлекли бы за собой неравенство Р ф ИР. Экспериментальные данные показывают, что современные ЗАТ-солверы могут выдавать корректный результат за приемлемое время на значительно больших выполнимых формулах, чем на невыполнимых. Несмотря на важность задачи существует не так много работ, в которых доказываются нижние оценки на время работы ОРЬЬ-алгоритмов на выполнимых формулах. Для других алгоритмов — основанных на локальном поиске — экспоненциальные нижние оценки для выполнимых формул известны довольно давно — с работ Гирша (2000) и Алехновича и Бен-Сассона (2002), также некоторые оценки были доказаны в работах Николенко (2003) и Бима (и др.) (2001). В работе Алехновича, Гирша и Ицыксона (2005) дается экспоненциальная нижняя оценка для двух достаточно больших классов ПРЫ^ алгоритмов — "близоруких" и "пьяных".

В работах Тревисана (и др.) (2009, 2014) и Ицыксона (2010) представлен "криптографический" взгляд на рассматриваемую проблему. Мы называем функцию / односторонней, если ее легко вычислить, но трудно обратить. Обычно принято считать, что функция легко вычислима, если она вычислима за полиномиальное время (из этого следует, что задача обращения функции лежит в классе КР). В 2000 году Голдрейх в своей работе предложил в качестве кандидата односторонней функции конструкцию, основанную на графах-экспандерах. Его конструкция принимает в качестве параметра двудольный

граф с п вершинами в каждой доле и степенью (I каждой вершины в правой доле (где й — некоторая константа, не зависящая от п или функция, растущая не быстрее 0(1с^(п))), а также предикат Р : {0,1}'г —> {0,1}. Для того, чтобы вычислить функцию на входе х е {0,1}", сопоставим биты входа вершинам из левой доли графа, после чего пометим каждую вершину в правой доле значением предиката Р, примененного к соседям вершины. Значением функции будет последовательность пометок вершин правой доли. В работе Трэвисана было замечено, что нижняя оценка для близоруких алгоритмов была доказана на формулах, которые кодируют задачу обращения функции Голдрейха с линейным предикатом. Однако линейная функция Голдрейха неинтересна с криптографической точки зрения, так как она быстро обращается при помощи метода Гаусса. Мотивацией в работе Трэвисана было доказательство нижней оценки для функции, которую, действительно трудно обратить. Как результат данной работы, была обобщена техника, разработанпая в работе Алехновича, Гирша и Ицыксона для доказательства нижней оценки для близоруких алгоритмов, на нелинейные предикаты и доказана экспоненциальная нижняя оценка на среднее (по входам функции) время обращения функции Голдрейха с предикатом х\ ф Х2 Ф • • • ©£<¿-2 Ф я<г-1 ха близорукими алгоритмами. Также было показано, что задача обращения функции Голдрейха с таким предикатом трудна для программы МшБАТ 2.0. Во всех перечисленных работах функция Голдрейха строится не явно, конструкция графа зависимостей вероятностная.

Все описанные нижние оценки на выполнимых формулах основаны на факте, что после нескольких шагов алгоритма формула станет трудной невыполнимой и алгоритм обойдет для нее все дерево расщепления. Однако, если разрешить алгоритму не просматривать некоторые ветви дерева, то никаких оценок не известно, в то время как такой подход кажется естественным для эвристических алгоритмов.

Формулы, которые кодируют невыполнимые системы линейных уравнений, сложны для ОРЬЬ-алгоритмов. В работе Алехновнча, Гирша и Ицык-сона показано, что выполнимые системы линейных уравнений также являются сложными примерами для близоруких и пьяных БРЬЬ-алгоритмов. Естественное обобщение ВРЬЬ-алгоритмов, которое может помочь решать линейные системы уравнений — алгоритмы, в которых расщепление происходит по линейной комбинации переменных над полем Кг. На текущий момент данные алгоритмы не исследованы, однако идеи подобного расщепления используются в теоретических алгоритмах для решения задачи выполнимости, в частности, в алгоритме Сето и Тамаки (2013).

Систематическое изучение вопросов, связанных с системами доказательств для пропозициональной логики, в частности, вопроса о длине минимального доказательства в различных системах, началось с работы Кука и Рекоу (1979). Интерес к этим вопросам обусловлен, в частности, тем, что пропозициональная система доказательств — это недетерминированный алгоритм, который определяет, является ли булева формула тавтологией (или невыполнимой формулой), таким образом неравенство NP ф со^Р влечет существование трудных примеров для всех систем доказательств. Следующий план иногда называют программой Кука: доказывать суперполиномиальные нижние оценки для все более сильных систем доказательств, пока не удастся развить методы, позволяющие обобщить результаты на произвольную систему доказательств.

Как было указано выше, для резолюционной системы доказательств существуют экспоненциальные нижние оценки. Однако, если разрешить вместо переменных использовать линейные комбинации над полем Рг, соответствующим образом преобразовав операции резолюционной системы доказательств, то получившая система будет не слабее классической резолюции, и на текущий момент нижних оценок на нее не известно. Также, как работа

БРЬЬ-алгорнтмов тесно связана, с резолюционной системой доказательств, работа алгоритмов расщепления по линейным уравнениям тесно связана с указанным обобщением резолюционной системы доказательств. Похожие системы доказательств рассматриваются в работе Раза и Цемерета (2008), однако в их работе рассматриваются линейные уравнения над целыми числами, а не над полем Рг-Цели работы.

1. Получить явную конструкцию графа и предиката, для которых функция Голдрейха является криптографически устойчивой по отношению к близоруким ОРЬЬ-алгоритмам. Доказать нижнюю оценку на время обращения данной функции.

2. Предложить обобщение ВРЬЬ-алгоритмов, добавив эвристику отсечения ветвей. Построить трудные примеры и доказать нижнюю оценку на время работы данного обобщения.

3. Построить двудольный граф-экспандер с ограниченной степенью вершин и полным рангом матрицы смежности.

4. Предложить схему алгоритмов расщепления по линейным функциям над полем F2 для решения задачи выполнимости. Доказать нижние и верхние оценки для данных алгоритмов.

5. Описать системы доказательств, связанные с алгоритмами расщепления но линейным функциям. Доказать нижние оценки для получепных систем доказательств.

Научная новизна. Все результаты диссертации являются новыми. Теоретическая и практическая ценность. Работа носит теоретический характер. Ее результаты могут быть использованы в структурной тео-

рии сложности и теории сложности в среднем для анализа алгоритмов, в теории сложности доказательств для получения оценок на различные системы доказательств. Конструкции графов-экспандеров могут быть использованы в различных областях дискретной математики и теории сложности.

Методы исследований. В работе используются методы теории сложности вычислений и доказательств, а также техника работы с графами-экспандерами. В частности, используются методы коммуникационной сложности, явные конструкции графов-экспандеров, строятся системы доказательств, используются методы расщепления. Основные результаты.

1. Получена явная конструкция такого графа-экспандера и предиката, что с вероятностью, близкой к 1, близорукие DPLL алгоритмы работают экспоненциальное время на формулах, кодирующих задачу обращения функции Голдрейха, основанной на данном графе и предикате.

2. Получена явная конструкция семейства таких невыполнимых формул

что для любого близорукого DPLL-алгоритма с эвристикой отсечения ветвей существует такой явный ансамбль распределений на выполнимых формулах Rn, что данный алгоритм либо ошибается на 99% формул, сгенерированных согласно распределению R„, либо работает экспоненциальное время па формуле

3. Получена явная конструкция двудольных графов-экспандеров, с ограниченной степенью вершин в обоих долях и полным рангом матрицы смежности над полем F2.

4. Построена модачь алгоритмов расщепления с расщеплением по линейным комбинациям переменных. Доказана полиномиальная верхняя оценка на время работы таких алгоритмов на формулах, кодирующих линейные системы уравнений. Доказана экспоненциальная нижняя

оценка на данную модель для 2-кратных цейтинских формул.

5. Описана система доказательств Res-Lin и Sem-Lin. Доказана их эквивалентность и семантическая полнота. Получена конструкция по дереву расщеплений древовидного доказательства в системе Res-Lin. Доказана экспоненциальная нижняя оценка на древовидные системы Res-Lin и Sem-Lin на 2-кратных цейтинских формулах.

Апробация работы. Результаты диссертационной работы были изложены на следующих конференциях и семинарах.

1. Международная конференция "The 6th International Computer Science Symposium in Russia" (Санкт-Петербург, CSR 2011).

2. Санкт-Петербургский городской семинар по дискретной математике.

3. Международная конференция "First Russian-Finnish Symposium on Discrete Mathematics" (Санкт-Петербург, RuFiDim 2011).

4. Колмогоровский семинар (Москва, 2011).

5. Международная конференция "The 22nd International Symposium on Algorithms and Computation" (Йокогама, ISAAC 2011).

G. Семинар по математической логике математического института города Прага (Прага, 2013).

7. Международный симпозиум "Franco-Russian workshop on Algorithms, complexity and applications" (Москва, 2013).

8. Международный симпозиум "Proof Complexity" (Вена, PC 2014).

9. Международная конференция "Mathematical Foundations of Computer Science 2014 - 39th International Symposium" (Будапешт, MFCS 2014).

Публикации. Основные результаты диссертации опубликованы в рецензируемых научных изданиях — [1], [2], [3], [4].

Работы [1]-[4] написаны в соавторстве. В работе [2] диссертанту принадлежат: конструкция графа-экспандера, достаточного для создания почти биективной функции Голдрейха (раздел 3); оценка на число прообразов функции Голдрейха после подстановок (леммы 5.6 и 5.7); реализация схемы доказательства, предложенной Ицыксоном в теоремах 5.1 и 5.2, эти же результаты приводятся в работе [1]. В работе [3] диссертанту принадлежат: конструкция по невыполнимой формуле семейства близоруких копий (лемма 3.1); упрощение понятия замыкания (раздел 4); доказательство свойств замыкания, предложенных Ицыксоном (предложение 4.1); конструкция экспандера с полным рангом матрицы смежности и ограниченной степенью вершин (лемма 5.1 и раздел 6); доказательство лемм 5.2 и 5.4, являющихся частью доказательства теоремы 5.1; доказательство, предложенной Ицыксоном теоремы о трудных распределениях на выполнимых формулах (теорема 5.3). В работе [4] диссертанту принадлежат: определение модели алгоритмов с расщеплением по линейным функциям, определение систем доказательств Res-Lin и Sem-Lin, результаты из раздела 4 о нижней оценке для 2-кратных цейтинских формул и результаты раздела 6 о системах доказательств Res-Lin и Sem-Lin.

Неупомянутые результаты работ принадлежат соавторам.

Структура и объем работы. Диссертация состоит из введения, четырех глав и списка литературы. Общий объем диссертации 88 страниц. Список литературы включает 51 наименование на 6 страницах.

Содержание работы

Во введении обсуждаются рассматриваемые в диссертации задачи, приводится обзор состояния исследований в области, формулируются основные

результаты диссертации, описывается структура диссертации.

В первой главе приведены основные определения и базовые теоремы, используемые в диссертации. В первом разделе дастся определение систем доказательств: согласно Куку системой доказательств для языка Ь называется полиномиальный по времени алгоритм П : {0,1}* х {0,1}* —> {0,1}, для которого выполнены следующие свойства:

• (полнота) если х £ Ь, то существует такой у, что II(ж, у) = 1;

• (корректность) если существует такой у, что П(а:, у) = 1, то х 6 Ь.

Также в первом разделе определяется резолюционная система доказательств. Во втором разделе дается определение общей схемы алгоритмов расщепления (БРЬЬ-алгоритмов). Алгоритм расщепления параметризован двумя эвристиками (процедурами):

• процедура А, которая по формуле в КНФ выдает переменную из этой формулы. Это переменная, по которой будет проводиться расщепление;

• процедура В, которая по формуле в КНФ и ее переменной выдает значение из {0,1}. Это значение, которое будет подставляться при расщеплении первым.

Алгоритм расщепления — это рекурсивный алгоритм, который получает на вход формулу </? и частичную подстановку р и работает следующим образом:

• Упростить (р с помощью правил упрощения (считаем, что правила упрощения меняют у? и р, причем все переменные, значения которых определяются подстановкой р, удаляются из формулы <р).

• Если формула стала пустой (т.е. все ее дизъюнкты выполнены подстановкой р), то выдать р. Если формула содержит пустой дизъюнкт (заведомо невыполнимый), то выдать «формула невыполнима».

• з := А(<р).

• с:= В (<рЛ).

• Запустить алгоритм рекурсивно на := с], {¿г,- := с}); если алгоритм выдал подстановку, то выдать ее, в противном случае рекурсивно запустить на := 1 — с], ри {х^ := 1 — с}); если рекурсивный вызов выдал подстановку, то выдать ее, иначе выдать «формула невыполнима».

Также во втором разделе первой главы определяются "пьяные" и "близорукие" ОРЬЬ-алгоритмы и показывается связь между алгоритмами расщепления и резолюционной системой доказательств. В третьем разделе дано определение функции Голдрейха и описано сведение задачи обращения функции к задаче выполнимости булевой формулы. В четвертом разделе дано определение графов-экспандеров и приведены примеры явных конструкций. В пятом разделе сформулировано понятие полиномиально моделируемого распределения на входах.

Вторая глава посвящена конструкции функции Голдрейха, обращение которой является трудной задачей для близоруких Б Р Ь Ь- ал го р и т м о в. Предлагаемая функция Голдрейха имеет следующую структуру: она состоит из суммы линейной функции Голдрейха и нелинейной. Линейная функция нужна для того, чтобы ОРЬЬ-алгоритмам было сложно ее обратить, а нелинейная нужна для того, чтобы получившаяся функция не была бы тривиально обратимой. Во втором разделе мы берем линейную функцию Голдрейха, основанную на экспандере и немного модифицируем ее для того, чтобы она стала почти биективной. Затем в разделе 2 мы доказываем нижнюю оценку на время работы близоруких ОРЬЬ-алгоритмов на невыполнимых формулах, полученных путем модификации формул, кодирующих задачу обращения. В третьем разделе мы определяем понятие "умного близорукого" алгоритма,

который сильнее, чем просто "близорукий", и показываем, что для функции, построенной по методу, описанному в разделе 1 с большой вероятностью за первые несколько шагов текущая формула станет невыполнимой, и применяем доказанную оценку для невыполнимых формул. Результатом главы 2 является следующая теорема.

Теорема 1. Для любого с > 0 существует такая явная конструкция нелинейной функции Голдрейха /, что для любого "близорукого" алгоритма А, выполнено Рг[£л(Ф/(х)=/(1,)) - > 1 — где Ьд(х) — время работы

алгоритма А на входе х, в — строка случайных битов, которые использует алгоритм А и К = п

В третьей главе класс ВРЬЬ-алгоритмов расширяется добавлением эвристику отсечения, которая может решить что ветвь дерева расщепления "бесперспективная" и не стоит ее просматривать. Цель данной главы — построение за полипомналыюе время семейства таких невыполнимых формул ф("), что для любых детерминированных эвристик А и С найдется такой полиномиально моделируемый ансамбль распределений П,п, что ВРЬЬ-алгоритм, основанный на эвристиках А, В и С для некоторой эвристики В либо ошибается на 99% формул, сгенерированных согласно распределению Яп, либо работает экспоненциальное время па формуле ф'*'.

В первом разделе дается формальное определение ВРЬЬ-алгоритмов с эвристикой отсечения ветвей. Во втором разделе для произвольной невыполнимой формулы Ф описывается достаточное свойство семейства выполнимых формул для доказательства искомой оценки, семейство формул, удовлетворяющее данному свойству назовем "система близоруких копий". В третьем разделе описывается вспомогательная конструкция замыкания. Данная конструкция является упрощением конструкции, предложенной Алехновичем н описанной в главе 2.

В четвертом разделе доказывается основная теорема данной главы.

Теорема 2. Существуют такой полиномиальный алгоритм, который выдает по п невыполнимую формулу фМ и такая константа 5 > 0, что для любого близорукого алгоритма с полиномиальными эвристиками А и С найдется такой полиномиально моделируемый ансамбль распределений Нп на выполнимых формулах, что если для некоторой эвристики В и некоторого б > О неравенство Рг [Ра,в,с(<?) = 1] > 1 — е выполнено, то время работы алгоритма Х>а,в>с(Ф^) не менее (1 — е)2м, где N = тт{п6, г/К},г = С1(п) и К — параметр близорукого алгоритма.

В первом параграфе данного раздела описывается конструкция семейства близоруких копий по формуле и алгоритму при помощи замыканий из раздела 3, данная конструкция основана на графах-экспандеров с дополнительными условиями, которая описана в разделе 5. Затем данная теорема обобщается с использованием стандартной техники и строится единое распределение, которое является трудным для всех алгоритмов. В конце раздела теорема 2 обобщается на случай трудных примеров, основанных па выполнимых формулах.

В пятом раздело описывается конструкция графов, необходимая для завершения доказательства из раздела 4.

Лемма 1. Для любого достаточно большого й и любого п существует явная конструкция (г, 0.75с?)-экспандера с размерами долей |Л"| = |У| = п, г = 0.(п) и со степенью вершин из доли X не более 20Ы, где к — достаточно большая константа.

В четвертой главе рассматривается обобщение БРЬЬ-алгоритмов на случай, когда допускается расщепление по линейным комбинациям переменных над полем Ег- В первом разделе главы дается формальное определение линейных деревьев расщеплений. Во втором разделе показывается, что при помощи линейных деревьев можно эффективно искать выполняющие наборы

для формул, кодирующих линейные системы уравнений. Заметим, что существуют такие системы линейных уравнений, для которых доказана нижняя оценка на время работы классических DPLL-алгоритмов. Также в разделе 2 показывается, что при помощи линейных деревьев расщеплений можно эффективно решать задачу выполнимости для формул, кодирующих существование совершенного паросочетання в графе с нечетным числом вершин.

В третьем разделе показывается связь между линейными деревьями расщеплений и коммуникационной сложностью задачи БеагсЬф — по подстановке значений переменным формулы ф найти опровергнутый дизъюнкт. Доказывается следующая теорема:

Теорема 3. Пусть ф — невыполнимая формула в КНФ и Т — линейное дерево расщеплений для ф. Тогда для любого распределения переменных между участниками коммуникационного протокола верно следующее утверждение: RT" (Searchф) = 0(log(|T|) loglog(|r|)).

3

Как следствие из дайной теоремы доказывается нижняя оценка па линейное дерево расщеплений для 2-кратных цейтинских формул.

Теорема 4. За полиномиальное от тг время можно построить граф G(V, Е) на п вершинах с максимальной степенью, ограниченной константой, и такую функцию с : V —> F2, что размер любого линейного дерева расщепления TSfGc) по крайней мере П (2"1/3/i°s3(")).

В разделе 4 приведено краткое доказательство нижней оценки на линейное дерево расщеплений для формул, кодирующих принцип Дирихле. В пятом разделе описываются системы доказательств Res-Lin и Sem-Lin, которые оперируют с линейными дизъюнктами — дизъюнкциями линейных уравнений. Показывается связь между линейными деревьями расщеплений и древовидной версией системы Res-Lin, таким образом нижние оценки на линейные деревья расщеплений переносятся на древовидную систему Res-Lin.

Затем в разделе 5 показывается эквивалентность систем Res-Lin и Sem-Lin, таким образом нижние оценки переносятся на древовидную версию системы Sem-Lin. В разделе 5.2 доказывается импликативная полнота систем Res-Lin и Sem-Lin, что позволяет перенести некоторые классические результаты, например, лемму о дедукции, на данные системы доказательств:

Теорема 5. Если линейный дизъюнкт Со семантически следует из Ci, Сг,..., Cjt, то Со может быть выведен из Ci, С'г, ..., С* в Res-Lin.

В разделе 5.3 доказывается, что система R(lin), описанная в работе Раза и Цемерета (2008) моделирует системы Res-Lin и Sem-Lin.

Публикации автора по теме диссертации в рецензируемых научных изданиях:

1. Itsykson Dmitry, Sokolov Dmitry. The Complexity of Inversion of Explicit Goldreich's Function by DPLL Algorithms // Computer Science — Theory and Applications / под ред. Alexander Kulikov, Nikolay Vereshchagin. Springer Berlin Heidelberg, 2011. T. 6651 из Lecture Notes in Computer Science. C. 134-147.

2. Ицыксон Дмитрий, Соколов Дмитрий. Сложность обращения явной функции Голдрейха DPLL алгоритмами // Записки научных семинаров ПОМИ. 2012. Т. 399. С. 88-108.

3. Itsykson Dmitry, Sokolov Dmitry. Lower Bounds for Myopic DPLL Algorithms with a Cut Heuristic // Algorithms and Computation / под ред. Takao Asano, Shin-ichi Nakano, Yoshio Okamoto [и др.]. Springer Berlin Heidelberg, 2011. T. 7074 из Lecture Notes in Computer Science. C. 464-473.

4. Itsykson Dmitry, Sokolov Dmitry. Lower Bounds for Splittings by Linear Combinations 11 Mathematical Foundations of Computer Science 2014 / под

ред. Erzsebet Csuhaj-Varju, Martin Dietzfelbinger, Zoltan Esik. Springer Berlin Heidelberg, 2014. T. 8635 из Lecture Notes in Computer Science. C. 372-383.

Другие публикации автора по теме диссертации:

5. Соколов Д. Нижние оценки на время работы DPLL алгоритмов с расщеплением по линейным функциям // Препринты ПОМИ РАН. Препринт 1/2014. 2014.

6. Itsykson Dmitry, Sokolov Dmitry. Lower bounds for myopic DPLL algorithms with a cut heuristic // Electronic Colloquium on Computational Complexity (ECCC). 2012. T. 19. C. 141.

Подписано в печать 20.01.2015 Формат 60x84 '/16 Цифровая Печ. л. 1.0 Тираж 100 Заказ №11/01 печать

Типография «Фапкон Принт» (197101, г. Санкт-Петербург, ул. Большая Пушкарская, д. 54, офис 2)