Распространение единицы

Единичное распространение ( UP ), или распространение логических ограничений ( BCP ), или однолитеральное правило ( OLR ) — это процедура автоматизированного доказательства теорем , которая может упростить набор (обычно пропозициональных ) предложений .

Определение

Процедура основана на единичных предложениях , т.е. предложениях, состоящих из одного литерала в конъюнктивной нормальной форме . Поскольку каждое предложение должно быть выполнено, мы знаем, что этот литерал должен быть истинным. Если набор предложений содержит предложение единицы $l$ остальные положения упрощаются за счет применения двух следующих правил:

каждое предложение (кроме самого единичного предложения), содержащее $l$ удаляется (условие выполняется, если $l$ является);
в каждом предложении, содержащем $\neg l$ этот литерал удаляется ( $\neg l$ не может способствовать его удовлетворению).

Применение этих двух правил приводит к появлению нового набора положений, эквивалентного старому.

Например, следующий набор предложений можно упростить за счет распространения единицы, поскольку он содержит предложение единицы. $a$ .

\{a\vee b,\neg a\vee c,\neg c\vee d,a\}

С $a\vee b$ содержит буквальный $a$ , этот пункт можно вообще убрать. С $\neg a\vee c$ содержит отрицание литерала в предложении единицы, этот литерал можно удалить из предложения. Пункт о единице $a$ не удаляется; это сделало бы результирующий набор не эквивалентным исходному; это предложение можно удалить, если оно уже сохранено в какой-либо другой форме (см. раздел «Использование частичной модели»). Эффект распространения единиц можно резюмировать следующим образом.

$\{$	$a\vee b,$	$\neg a\vee c,$	$\neg c\vee d,$	$a$	$\}$
	(удаленный)	( $\neg a$ удалено)	(без изменений)	(без изменений)
$\{$		$c,$	$\neg c\vee d,$	$a$	$\}$

Полученный набор предложений $\{c,\neg c\vee d,a\}$ эквивалентно предыдущему. Новое положение о единице измерения $c$ который является результатом единичного распространения, может быть использован для дальнейшего применения единичного распространения, которое преобразует $\neg c\vee d$ в $d$ .

Распространение и разрешение единицы измерения

Второе правило распространения единиц можно рассматривать как ограниченную форму разрешения , в которой одна из двух резольвент всегда должна быть предложением единицы. Что касается разрешения, распространение единиц является правильным правилом вывода, поскольку оно никогда не создает нового предложения, которое не было бы повлечено за собой старыми. Различия между распространением единицы измерения и разрешением:

разрешение представляет собой полную процедуру опровержения, а распространение единицы - нет; другими словами, даже если набор предложений противоречив, распространение единиц не может привести к несогласованности;
два разрешенных предложения, как правило, не могут быть удалены после добавления сгенерированного предложения в набор; напротив, предложение без единицы, участвующее в распространении единицы, может быть удалено, когда к набору добавляется его упрощение;
разрешение обычно не включает первое правило, используемое при распространении единиц.

Исчисления разрешения, включающие разделение, могут моделировать первое правило путем включения, а правило два - с помощью шага единичного разрешения, за которым следует разделение.

Распространение единиц, применяемое неоднократно по мере генерации новых единичных предложений, представляет собой полный алгоритм выполнимости для наборов пропозициональных предложений Хорна ; он также генерирует минимальную модель для набора, если она выполнима: см. Хорн-выполнимость .

Использование частичной модели

Предложения модуля, которые присутствуют в наборе предложений или могут быть получены из него, могут храниться в форме частичной модели (эта частичная модель может также содержать другие литералы, в зависимости от приложения). В этом случае распространение единицы выполняется на основе литералов частичной модели, а предложения единиц удаляются, если их литерал присутствует в модели. В приведенном выше примере предложение unit $a$ будет добавлен в частичную модель; тогда упрощение набора предложений будет происходить, как указано выше, с той разницей, что единичное предложение $a$ теперь удален из набора. Результирующий набор предложений эквивалентен исходному при условии допустимости литералов в частичной модели.

Сложность

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

Однако распространение единиц можно осуществлять за линейное время, сохраняя для каждой переменной список предложений, в которых содержится каждый литерал. Например, приведенный выше набор можно представить, пронумеровав каждое предложение следующим образом:

\{1:a\vee b,2:\neg a\vee c,3:\neg c\vee d,4:a\}

а затем сохраняем для каждой переменной список предложений, содержащих переменную или ее отрицание:

a:1\ 2\ 4

b:1

c:2\ 3

d:3

Эта простая структура данных может быть построена линейно по размеру набора и позволяет очень легко находить все предложения, содержащие переменную. Распространение литерала по единицам можно эффективно выполнить, просматривая только список предложений, содержащих переменную литерала. Точнее, общее время выполнения единичного распространения для всех единичных предложений линейно зависит от размера набора предложений.

См. также

Ссылки

Даулинг, Уильям Ф.; Галлиер, Жан Х. (1984), «Алгоритмы линейного времени для проверки выполнимости пропозициональных формул Хорна», Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016/0743-1066(84)90014- 1 , МР 0770156 .
Х. Чжан и М. Стикель (1996). Эффективный алгоритм единичного распространения. В материалах Четвертого Международного симпозиума по искусственному интеллекту и математике .