Резолюция - это схема, доказывающая неудовлетворенность CNF. Доказательством в резолюции является логический вывод пустого предложения для начальных предложений в CNF. В частности, любой начальный пункт может быть выведен, и из двух пунктов и B ∨ ¬ x также может быть выведен пункт A ∨ B. Опровержение - это последовательность выводов, которая заканчивается пустым предложением.
Если такое опровержение будет реализовано, мы можем рассмотреть процедуру, которая хранит некоторые пункты в памяти. В случае, если не начальное предложение должно использоваться снова, и оно больше не находится в памяти, алгоритм должен должен это снова с нуля или от тех в памяти.
Пусть наименьшее количество предложений, которые должны храниться в памяти, чтобы достичь пустых предложений. Это называется раздел пространства сложность . Скажем, что является выполнимым.
Проблема, которую я предлагаю, заключается в следующем: рассмотрим два CNF и B = ⋀ n j = 1 B j , и пусть CNF
Какова связь с и ?
Очевидной верхней границей является . Это туго?
источник
Ответы:
Я хотел опубликовать это как комментарий, но так как я не могу понять, как это сделать, я думаю, что вместо этого это будет «ответ».
Я согласен, что вопрос хороший. Конечно, тот же вопрос может быть задан и относительно длины опровержений разрешения (т. Е. Количества пунктов, встречающихся в опровержении, подсчитанных с повторениями) и ширины опровержения (т. Е. Размера или числа литералов, встречающихся в , самая большая оговорка в опровержении).
Во всех этих случаях существуют «очевидные» верхние границы, но мне не ясно, следует ли ожидать совпадения нижних границ или нет. Поэтому я хотел добавить один вопрос и один комментарий.
Вопрос касается длины опровержения. Кажется разумным полагать, что ограничение длины, указанное в комментарии Массимо, является жестким, но знаем ли мы это?
Это, конечно, легкое наблюдение, но дело в том, что это может указывать на то, что вопрос о космосе может быть сложным. Это так, поскольку почти все нижние границы пространства в опровержении, о которых мы знаем, проходят через нижние границы ширины. (То есть нижние границы пространства были получены независимо, но, оглядываясь назад, все они следуют в качестве следствия из красивой статьи «Комбинаторная характеристика ширины разрешения» Ацериаса и Далмау.) Но если для предложения по разрешению есть теорема о прямой сумме пространство, оно не будет следовать из нижних границ ширины, но должно обсуждаться напрямую, что, по крайней мере, до сих пор казалось гораздо сложнее. Но, конечно, может быть какой-то простой аргумент, который я пропускаю.
источник