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

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

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

При наличии доказательства невыполнимости и переменной легко перестроить (разделить) доказательство на доказательство и доказательство , а рекомбинация этих двух доказательств (путем дополнительного шага разрешения) может привести к доказательству, меньшему, чем исходное.${\displaystyle \пи}$${\displaystyle x}$${\displaystyle x}$${\displaystyle \отрицательный x}$

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

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

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

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

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

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

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

${\displaystyle \pi _{l}(c):={\begin{cases}c,&{\text{if }}c{\text{ is 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{ и }}\neg x\in \pi _{l}(n)\end{cases}}}$

Также пусть будет пустым предложением в . Тогда и получаются путем вычисления и , соответственно.${\displaystyle о}$${\displaystyle \пи}$${\displaystyle \пи _{x}}$${\displaystyle \пи _{\отрицательный x}}$${\displaystyle \пи _{x}(o)}$${\displaystyle \пи _{\отрицательный х}(о)}$