Теорема о прямой сумме для пространственной сложности предложения Резолюции?

10

Резолюция - это схема, доказывающая неудовлетворенность CNF. Доказательством в резолюции является логический вывод пустого предложения для начальных предложений в CNF. В частности, любой начальный пункт может быть выведен, и из двух пунктов и B ¬ x также может быть выведен пункт A B. Опровержение - это последовательность выводов, которая заканчивается пустым предложением.AxB¬xAB

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

Пусть Sp(F) наименьшее количество предложений, которые должны храниться в памяти, чтобы достичь пустых предложений. Это называется раздел пространства сложность F . Скажем, что Sp(F)= является F выполнимым.

Проблема, которую я предлагаю, заключается в следующем: рассмотрим два CNF и B = n j = 1 B j , и пусть CNFA=i=1mAiB=j=1nBj

AB=i=1mj=1nAiBj

Какова связь Sp(AB) с Sp(A) и Sp(B) ?

Очевидной верхней границей является Sp(AB)Sp(A)+Sp(B)1 . Это туго?

MassimoLauria
источник
Хороший вопрос! Вы знаете ответ по размеру прямой суммы? Я предполагаю, что худший случай, когда A и B не имеют общих переменных. Интересный случай может быть, когда A и B одинаковы вплоть до переименования переменной. Кстати, я не вижу, как вы получаете эту верхнюю границу, кажется, что это может быть намного хуже.
Каве
BAiBj1jnAi1imAm.(Size(B)+O(1))+Size(A),
Каве
F1F2FkFiF
1
Length(AB)Length(B)|A|+Length(A)
Верхняя граница тривиального пространства на самом деле требует еще одного предложения в памяти. Я отредактировал соответственно.
MassimoLauria

Ответы:

7

Я хотел опубликовать это как комментарий, но так как я не могу понять, как это сделать, я думаю, что вместо этого это будет «ответ».

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

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

Вопрос касается длины опровержения. Кажется разумным полагать, что ограничение длины, указанное в комментарии Массимо, является жестким, но знаем ли мы это?

ABiwABBwBmax(wA,wB)

Это, конечно, легкое наблюдение, но дело в том, что это может указывать на то, что вопрос о космосе может быть сложным. Это так, поскольку почти все нижние границы пространства в опровержении, о которых мы знаем, проходят через нижние границы ширины. (То есть нижние границы пространства были получены независимо, но, оглядываясь назад, все они следуют в качестве следствия из красивой статьи «Комбинаторная характеристика ширины разрешения» Ацериаса и Далмау.) Но если для предложения по разрешению есть теорема о прямой сумме пространство, оно не будет следовать из нижних границ ширины, но должно обсуждаться напрямую, что, по крайней мере, до сих пор казалось гораздо сложнее. Но, конечно, может быть какой-то простой аргумент, который я пропускаю.

Якоб Нордстрем
источник
2
Добро пожаловать, Якоб!
Арнаб
1
К сожалению, комментарии ограничены людьми с репутацией не менее 50 - это странность программного обеспечения и связано с предотвращением спама. Я уверен, что вы быстро пересечете этот порог.
Суреш Венкат
Привет, Джейкоб, приятно видеть тебя здесь. (ps: я думаю, что вы преодолели порог.)
Kaveh
Привет, Джейкоб, мне интересно, есть ли у такого рода заявления какие-то последствия в отношении компромиссов. В качестве метода нижней границы, который не был бы очень мощным инструментом: длина формулы квадратируется, а пространство увеличивается линейно. В любом случае это свойство может привести к формуле с небольшой шириной и большим пространством (обратите внимание, что ширина также увеличивается, если выполняется непостоянное число повторений).
MassimoLauria