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

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

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

1. каждое предложение (кроме самого предложения единицы), содержащее удаляется (предложение удовлетворено, если есть);${\displaystyle л}$${\displaystyle л}$
2. в каждом предложении, содержащем этот литерал, удаляется ( не может способствовать его удовлетворению).${\displaystyle \отрицательный л}$${\displaystyle \отрицательный л}$

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

Например, следующий набор предложений можно упростить путем распространения единиц, поскольку он содержит предложение единицы .${\displaystyle а}$

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

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

${\displaystyle \{}$	${\displaystyle а\ве б,}$	${\displaystyle \neg a\vee c,}$	${\displaystyle \neg c\vee d,}$	${\displaystyle а}$	${\displaystyle \}}$
	(удаленный)	( удалено)${\displaystyle \отрицательный а}$	(без изменений)	(без изменений)
${\displaystyle \{}$		${\displaystyle с,}$	${\displaystyle \neg c\vee d,}$	${\displaystyle а}$	${\displaystyle \}}$

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

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

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

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

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

В этом разделе не указаны источники . Помогите улучшить этот раздел , добавив ссылки на надежные источники . Материалы без ссылок могут быть оспорены и удалены . ( Декабрь 2023 г. ) ( Узнайте, как и когда удалять это сообщение )

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

В этом разделе не указаны источники . Помогите улучшить этот раздел , добавив ссылки на надежные источники . Материалы без ссылок могут быть оспорены и удалены . ( Декабрь 2023 г. ) ( Узнайте, как и когда удалять это сообщение )

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

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

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

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

${\displaystyle а:1\ 2\ 4}$

${\displaystyle б:1}$

${\displaystyle c:2\ 3}$

${\displaystyle д:3}$

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

• Роговая выполнимость
• Оговорка Хорна
• Автоматизированное доказательство теорем
• алгоритм DPLL

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