Сжатие с подтверждением разрешения путем разделения

В математической логике сжатие доказательства путем разделения — это алгоритм , который действует как постобработка доказательств разрешения . Это было предложено Скоттом Коттоном в его статье «Два метода минимизации доказательства разрешения». ^[1]

Алгоритм разделения основан на следующем наблюдении:

Учитывая доказательство невыполнимости $\pi$ и переменная $x$ , то легко перестроить (разбить) доказательство на доказательство $x$ и доказательство $\neg x$ и рекомбинация этих двух доказательств (с помощью дополнительного шага разрешения) может привести к получению доказательства меньшего размера, чем оригинал.

Обратите внимание, что применение расщепления в доказательстве $\pi$ используя переменную $x$ не делает недействительным последнее применение алгоритма с использованием другой переменной $y$ . Собственно, метод, предложенный Коттоном ^[1] генерирует последовательность доказательств $\pi _{1}\pi _{2}\ldots$ , где каждое доказательство $\pi _{i+1}$ является результатом применения разделения к $\pi _{i}$ . При построении последовательности, если доказательство $\pi _{j}$ оказывается слишком большим, $\pi _{j+1}$ считается наименьшим доказательством в $\{\pi _{1},\pi _{2},\ldots ,\pi _{j}\}$ .

Для достижения лучшего соотношения сжатия/времени желательна эвристика выбора переменных. Для этой цели Коттон ^[1] определяет «аддитивность» шага разрешения (с антецедентами $p$ и $n$ и решительный $r$ ):

\operatorname {add} (r):=\max(|r|-\max(|p|,|n|),0)

Тогда для каждой переменной $v$ , оценка рассчитывается как сумма аддитивности всех шагов разрешения в $\pi$ с шарниром $v$ вместе с количеством этих шагов разрешения. Обозначая каждую оценку, рассчитанную таким образом, через $add(v,\pi )$ , каждая переменная выбирается с вероятностью, пропорциональной ее баллу:

p(v)={\frac {\operatorname {add} (v,\pi _{i})}{\sum _{x}{\operatorname {add} (x,\pi _{i})}}}

Чтобы разделить доказательство невыполнимости $\pi$ в доказательстве $\pi _{x}$ из $x$ и доказательство $\pi _{\neg x}$ из $\neg x$ , Хлопок ^[1] предлагает следующее:

Позволять $l$ обозначают литерал и $p\oplus _{x}n$ обозначим резольвенту предложений $p$ и $n$ где $x\in p$ и $\neg x\in n$ . Затем определите карту $\pi _{l}$ на узлах в разрешении dag $\pi$ :

\pi _{l}(c):={\begin{cases}c,&{\text{if }}c{\text{ is an input}}\\\pi _{l}(p),&{\text{if }}c=p\oplus _{x}n{\text{ and }}(l=x{\text{ or }}x\notin \pi _{l}(p))\\\pi _{l}(n),&{\text{if }}c=p\oplus _{x}n{\text{ and }}(l=\neg x{\mbox{ or }}\neg x\notin \pi _{l}(n))\\\pi _{l}(p)\oplus _{x}\pi _{l}(p),&{\text{if }}x\in \pi _{l}(p){\text{ and }}\neg x\in \pi _{l}(n)\end{cases}}

Кроме того, пусть $o$ быть пустым предложением в $\pi$ . Затем, $\pi _{x}$ и $\pi _{\neg x}$ получаются путем вычисления $\pi _{x}(o)$ и $\pi _{\neg x}(o)$ , соответственно.

Примечания

^ Jump up to: ^а ^б ^с ^д Коттон, Скотт. «Два метода минимизации доказательств разрешения». 13-я Международная конференция по теории и приложениям проверки выполнимости, 2010 г.

[Cotton-1] Jump up to: ^а ^б ^с ^д Коттон, Скотт. «Два метода минимизации доказательств разрешения». 13-я Международная конференция по теории и приложениям проверки выполнимости, 2010 г.

[1]