Нижние оценки для ветвящихся программ с ограниченными повторениями на задачи поиска

Бесплатно
Работа доступна по лицензии Creative Commons:«Attribution» 4.0
Софронова Анастасия Александровна
Бесплатно
Работа доступна по лицензии Creative Commons:«Attribution» 4.0

Ветвящиеся программы позволяют описать различные меры сложности, например, память в машинах Тьюринга или длину доказательств в пропозициональных системах доказательств. В данной работе изучается связь именно с системами доказательств, впервые описанная Ловасом и др. ’95, которые показали, что регулярная резолюция эквивалентна однопроходным ветвящимся программам для задачи поиска невыполненного клоза. Эта связь широко используется; например, в недавнем результате о сложности клики в регулярной резолюции (Атсериас и др. ’18).

Мы изучаем ветвящиеся программы с ограниченными повторениями, так называемые (1, +k)-BP (Силинг ’96), в применении к задаче поиска невыполненного клоза (Search Phi). С одной стороны, это естественное обобщение однопроходных ветвящихся программ. С другой стороны, данная модель вычислений соответствует довольно сильной системе доказательств, в которой существуют короткие доказательства для широкого класса формул, сложных для резолюции (Кноп ’17).

Мы работаем с задачей Search Phi, которая является “простой” в сравнении с известными сложными примерами для (1, +k)-BP. В работе представлена первая техника для доказательства экспоненциальных нижних оценок на (1, +k)-BP для задачи Search Phi. Для этого мы объединяем известную технику для доказательств нижних оценок на ветвящиеся программы (Силинг ’96; Силинг, Вегенер ’94; Юкна, Разборов ’98) с модификацией техники “замыкания” (Алехнович и др. ’04; Алехнович, Разборов ’03). В отличие от большинства нижних оценок на резолюцию, наша техника использует не только локальные свойства формулы, но и её глобальную структуру. Сложное семейство формул, описанное в работе, основано на потоковых формулах, описанных в (Алехнович, Разборов ’03).

1. Introduction 3
1.1. Ourresults……………………………….. 5
1.2. Technique ……………………………….. 5
2. Preliminaries 7
2.1. Branchingprograms…………………………… 7
3. Expanders 10
4. Lower bounds for (1, + )-BP 12
4.1. HardFormulas……………………………… 13
4.1.1. LocallyConsistentAssignments…………………. 15
4.2. ProofofTheorem1.4 ………………………….. 16
4.2.1. ConstructionoftheGarland…………………… 17
4.3. UnreachableLeaves…………………………… 20
4.4. DirectingtheFlow……………………………. 22
5. Conclusion 28
References 29
A. MissedLemmas 32
A.1.Lemma4.5……………………………….. 32
A.2. Lemma4.10 ………………………………. 35
B. Garland in the Paths 38

Propositional proof complexity theory studies proof systems for UNSAT, the language of unsatisfiable propositional formulas. Studying lower bounds on size of such proofs is closely related to the question whether NP and coNP coincide or not. Non-equivalence of those classes would be equivalent to existence of hard formulas for any propositional proof system — that is, formulas which do not have short, polynomial-size proofs.
There exists so-called Cook’s program, which proposes to prove superpolynomial lower bounds for stronger and stronger proof systems until the techniques are developed to do it in a general case. Currently there exist lower bounds only for some specific proof systems.
For many proof systems, the proofs describe the runs of specific classes of SAT-solving al- gorithms. Which means that lower bounds of the size of proofs give us lower bounds on run- ning time of SAT- solvers, as well as some other algorithms. For example, Resolution describes DPLL algorithms [DLL62; Gol79], Cutting Planes corresponds to combinatorial optimization [Gom58; Gom60; Gom63], Nullstellensatz and Polynomial Calculus are related to calculating Gröbner basis [CEI96; Bus+97]. For all those systems there are known lower bounds. The majority of theorem-proving systems is based on propositional proofs as well.
Proofs of unsatisfiability of a formula are closely connected to a certain search relation: given an assignment, it is required to find an unsatisfied clause. Formally it is defined in the following way:

Definition 1.2
An unsatisfied clause search problem Search for an unsatisfiable CNF formula ≔ ⋀ on variables is defined as follows:

input: an -variable assignment ∈ {0, 1} ;
output: an element ∈ such that clause of is falsified by .
Informally speaking, we may think that if we can solve the Search problem in some computational model C, then the description of ∈ C that solves Search is a “certificate of unsatisfiability” of a formula . So we may think of this model as a proof system.
We study a computational model named branching programs. A proof system based on 3
this model could be defined in a way described above [Kno17]. Regular Resolution, which is the restriction of general Resolution, is, in those terms, equivalent to a read-once branching program that searches for an unsatisfied clause [Lov+95].
Branching program is a computational model that is described by a directed acyclic graph. In each vertex a variable is queried, and we proceed along one of the outgoing edges depending on its value. A total assignment corresponds to a path from source to one of the sinks (a computation path), and in the sink a value of a function is written. Let us state the formal definition.
Definition 1.3
Let ≔ { 1, … , } be a set of propositional variables and be a finite set.
A branching program for a relation ⊆ {0, 1} × is a directed acyclic graph with one source. Every sink of the graph is labeled with ∈ , every inner vertex is
labeled with ∈ and it has exactly two outgoing edges labeled by 0 and 1.
Every total assignment : → {0, 1} to variables induces a path in a branch- ing program in the following way. We start in the root of the program. If the current
vertex is labeled with variable , we proceed along the edge ( ).
Let ∈ be the label in the sink we ended up in. We require the following property:
( ( 1), … , ( ), ) ∈ .
This is one of the most fundamental models in theoretical computer science: it captures the space complexity of many versions of restricted and unrestricted Turing machine etc. The read-once version queries each bit only once on every path. This model corresponds to the eraser Turing machines. Exponential lower bounds for this model were proven in [Weg88; Žák86].
The connection between regular Resolution and branching programs makes it interesting to consider some less restricted models of branching programs in application to the Search problems. Some of these models were considered in [Kno17]. In this paper we focus on (1, + )-BPs (branching programs with bounded repetitions).
It is a natural generalization of read-once branching programs that was described in [Sie96]. In this model, we allow our branching programs to requery variables, but on each computation only input bits may be queried more than one time. There are two natural points of view on this model:
syntactic: if we apply the restriction on every path;
semantic: if we apply the restriction on consistent paths
(for formal definition see section 2.1). The semantic version is more powerful and may capture
strong Turing machine models (for details see [JR98]). 4

Exponential lower bounds on (1, + )-BP were shown in [SŽ97; Sie96; SW94; JR98] for various parameters . Lower bounds from [JR98] hold for = Ω ( ) and the lower bound
log
from [Juk08] holds even for = Ω( ), where is the number of input bits. We refer the
reader to the books [Juk12; Weg00] with the detailed description of results related to branching programs.
Described lower bounds for (1, + )-BP are given for “complicated” functions (usually it is characteristic functions of an error-correcting code with additional properties). In particular, these functions are complicated in terms of the certificate complexity, which is not true for Search relation, so the usual techniques do not work in this case. Despite the success in proving lower bounds on the Resolution (and hence read-once programs) the lower bounds for (1, + )-BP on the Search are an open question even for = 1.
Apart from small certificate complexity, there arises another issue in proving lower bounds on Search . It is that (1, + )-BP is much stronger than general Resolution on some classes of formulas [Kno17] even for small constant and syntactic model. This is a crucial observation and it means that we cannot directly apply general techniques for proving lower bounds in proof complexity like [BW01; AR03] etc., since these techniques cannot distinguish between considered classes of formulas and other hard examples for Resolution. Hence if we want to prove lower bound for (1, + )-BP on Search we need some additional arguments in comparison to Resolution lower bounds.
In this work, we introduce a technique for proving such lower bounds on the semantic (1, + )-BP where = (log / log log ) where is the number of variables.
1.1 Our results
The main result is an exponential lower bound on the size of (1, + )-BPs in application
to Search

for = ( log ). log log

Заказать новую

Лучшие эксперты сервиса ждут твоего задания

от 5 000 ₽

Не подошла эта работа?
Закажи новую работу, сделанную по твоим требованиям

    Нажимая на кнопку, я соглашаюсь на обработку персональных данных и с правилами пользования Платформой

    Читать «Нижние оценки для ветвящихся программ с ограниченными повторениями на задачи поиска»

    Последние выполненные заказы

    Хочешь уникальную работу?

    Больше 3 000 экспертов уже готовы начать работу над твоим проектом!

    Екатерина Д.
    4.8 (37 отзывов)
    Более 5 лет помогаю в написании работ от простых учебных заданий и магистерских диссертаций до реальных бизнес-планов и проектов для открытия своего дела. Имею два об... Читать все
    Более 5 лет помогаю в написании работ от простых учебных заданий и магистерских диссертаций до реальных бизнес-планов и проектов для открытия своего дела. Имею два образования: экономист-менеджер и маркетолог. Буду рада помочь и Вам.
    #Кандидатские #Магистерские
    55 Выполненных работ
    Мария Б. преподаватель, кандидат наук
    5 (22 отзыва)
    Окончила специалитет по направлению "Прикладная информатика в экономике", магистратуру по направлению "Торговое дело". Защитила кандидатскую диссертацию по специальнос... Читать все
    Окончила специалитет по направлению "Прикладная информатика в экономике", магистратуру по направлению "Торговое дело". Защитила кандидатскую диссертацию по специальности "Экономика и управление народным хозяйством". Автор научных статей.
    #Кандидатские #Магистерские
    37 Выполненных работ
    Кирилл Ч. ИНЖЭКОН 2010, экономика и управление на предприятии транс...
    4.9 (343 отзыва)
    Работы пишу, начиная с 2000 года. Огромный опыт и знания в области экономики. Закончил школу с золотой медалью. Два высших образования (техническое и экономическое). С... Читать все
    Работы пишу, начиная с 2000 года. Огромный опыт и знания в области экономики. Закончил школу с золотой медалью. Два высших образования (техническое и экономическое). Сейчас пишу диссертацию на соискание степени кандидата экономических наук.
    #Кандидатские #Магистерские
    692 Выполненных работы
    Анна С. СФ ПГУ им. М.В. Ломоносова 2004, филологический, преподав...
    4.8 (9 отзывов)
    Преподаю англ язык более 10 лет, есть опыт работы в университете, школе и студии англ языка. Защитила кандидатскую диссертацию в 2009 году. Имею большой опыт написания... Читать все
    Преподаю англ язык более 10 лет, есть опыт работы в университете, школе и студии англ языка. Защитила кандидатскую диссертацию в 2009 году. Имею большой опыт написания и проверки (в качестве преподавателя) контрольных и курсовых работ.
    #Кандидатские #Магистерские
    16 Выполненных работ
    Петр П. кандидат наук
    4.2 (25 отзывов)
    Выполняю различные работы на заказ с 2014 года. В основном, курсовые проекты, дипломные и выпускные квалификационные работы бакалавриата, специалитета. Имею опыт напис... Читать все
    Выполняю различные работы на заказ с 2014 года. В основном, курсовые проекты, дипломные и выпускные квалификационные работы бакалавриата, специалитета. Имею опыт написания магистерских диссертаций. Направление - связь, телекоммуникации, информационная безопасность, информационные технологии, экономика. Пишу научные статьи уровня ВАК и РИНЦ. Работаю техническим директором интернет-провайдера, имею опыт работы ведущим сотрудником отдела информационной безопасности филиала одного из крупнейших банков. Образование - высшее профессиональное (в 2006 году окончил военную Академию связи в г. Санкт-Петербурге), послевузовское профессиональное (в 2018 году окончил аспирантуру Уральского федерального университета). Защитил диссертацию на соискание степени "кандидат технических наук" в 2020 году. В качестве хобби преподаю. Дисциплины - сети ЭВМ и телекоммуникации, информационная безопасность объектов критической информационной инфраструктуры.
    #Кандидатские #Магистерские
    33 Выполненных работы
    Анна В. Инжэкон, студент, кандидат наук
    5 (21 отзыв)
    Выполняю работы по экономическим дисциплинам. Маркетинг, менеджмент, управление персоналом. управление проектами. Есть опыт написания магистерских и кандидатских диссе... Читать все
    Выполняю работы по экономическим дисциплинам. Маркетинг, менеджмент, управление персоналом. управление проектами. Есть опыт написания магистерских и кандидатских диссертаций. Работала в маркетинге. Практикующий бизнес-консультант.
    #Кандидатские #Магистерские
    31 Выполненная работа
    Дмитрий М. БГАТУ 2001, электрификации, выпускник
    4.8 (17 отзывов)
    Помогаю с выполнением курсовых проектов и контрольных работ по электроснабжению, электроосвещению, электрическим машинам, электротехнике. Занимался наукой, писал стать... Читать все
    Помогаю с выполнением курсовых проектов и контрольных работ по электроснабжению, электроосвещению, электрическим машинам, электротехнике. Занимался наукой, писал статьи, патенты, кандидатскую диссертацию, преподавал. Занимаюсь этим с 2003.
    #Кандидатские #Магистерские
    19 Выполненных работ
    Дмитрий К. преподаватель, кандидат наук
    5 (1241 отзыв)
    Окончил КазГУ с красным дипломом в 1985 г., после окончания работал в Институте Ядерной Физики, защитил кандидатскую диссертацию в 1991 г. Работы для студентов выполня... Читать все
    Окончил КазГУ с красным дипломом в 1985 г., после окончания работал в Институте Ядерной Физики, защитил кандидатскую диссертацию в 1991 г. Работы для студентов выполняю уже 30 лет.
    #Кандидатские #Магистерские
    2271 Выполненная работа
    Катерина В. преподаватель, кандидат наук
    4.6 (30 отзывов)
    Преподаватель одного из лучших ВУЗов страны, научный работник, редактор научного журнала, общественный деятель. Пишу все виды работ - от эссе до докторской диссертации... Читать все
    Преподаватель одного из лучших ВУЗов страны, научный работник, редактор научного журнала, общественный деятель. Пишу все виды работ - от эссе до докторской диссертации. Опыт работы 7 лет. Всегда на связи и готова прийти на помощь. Вместе удовлетворим самого требовательного научного руководителя. Возможно полное сопровождение: от статуса студента до получения научной степени.
    #Кандидатские #Магистерские
    47 Выполненных работ

    Другие учебные работы по предмету

    Алгоритмы для динамических диаграмм Вороного
    📅 2021 год
    🏢 Санкт-Петербургский государственный университет
    О локальных свойствах решений задач гидродинамики
    📅 2021 год
    🏢 Санкт-Петербургский государственный университет
    Структуры комодулей на кольцах Чжоу флаговых многообразий
    📅 2021 год
    🏢 Санкт-Петербургский государственный университет
    Полнота биортогональных систем для нескольких интервалов
    📅 2021 год
    🏢 Санкт-Петербургский государственный университет
    Задача размещения элементов цепи поставок
    📅 2021 год
    🏢 Санкт-Петербургский государственный университет