Распространение Unit ( UP ) или распространение Логического Constraint ( BCP ) или один литерал правило ( OLR ) представляет собой процедуру из автоматического доказательства , что позволяет упростить набор (обычно пропозициональные ) положений .
Определение
Процедура основана на единичных предложениях , то есть предложениях, которые состоят из одного литерала . Поскольку каждое предложение должно быть выполнено, мы знаем, что этот литерал должен быть истинным. Если набор предложений содержит предложение unit, остальные пункты упрощаются применением двух следующих правил:
- каждое предложение (кроме самого предложения модуля), содержащее удаляется (условие выполняется, если является);
- в каждом пункте, содержащем этот литерал удален ( не могу поспособствовать тому, чтобы быть довольным).
Применение этих двух правил приводит к новому набору пунктов, который эквивалентен старому.
Например, следующий набор предложений можно упростить путем распространения единицы, поскольку он содержит предложение единицы .
С содержит буквальный , этот пункт можно полностью исключить. Ссодержит отрицание литерала в предложении единицы, этот литерал может быть удален из предложения. Оговорка о единицахне снимается; это сделало бы результирующий набор не эквивалентным исходному; это предложение может быть удалено, если оно уже сохранено в какой-либо другой форме (см. раздел «Использование частичной модели»). Эффект единичного распространения можно резюмировать следующим образом.
(удаленный) | ( удалено) | (без изменений) | (без изменений) | ||
Результирующий набор предложений эквивалентен приведенному выше. Новая статья о единицах который является результатом единичного распространения, может быть использован для дальнейшего применения единичного распространения, что преобразует в .
Распространение и разрешение единицы
Второе правило распространения единиц можно рассматривать как ограниченную форму разрешения , в которой одна из двух резольвент всегда должна быть предложением единицы. Что касается разрешения, распространение единиц является правильным правилом вывода, поскольку оно никогда не приводит к появлению нового предложения, которое не влечет за собой старые. Различия между единичным распространением и разрешением:
- разрешение - это процедура полного опровержения, а распространение единиц - нет; другими словами, даже если набор предложений противоречив, распространение единиц не может вызвать несогласованность;
- два разрешенных предложения, как правило, не могут быть удалены после добавления сгенерированного предложения в набор; напротив, предложение non-unit, участвующее в распространении единицы, может быть удалено, когда его упрощение добавлено к набору;
- разрешение, как правило, не включает первое правило, используемое при распространении единиц измерения.
Исчисления разрешающей способности, которые включают в себя отнесение, могут моделировать первое правило посредством отнесения и правило два с помощью шага разрешения единицы, за которым следует отнесение.
Распространение единиц, применяемое неоднократно по мере создания новых единичных предложений, представляет собой алгоритм полной выполнимости для наборов пропозициональных предложений Хорна ; он также генерирует минимальную модель для множества, если выполнимо: см. Выполнимость по Хорну .
Использование частичной модели
Предложения модуля, которые присутствуют в наборе предложений или могут быть производными от него, могут быть сохранены в форме частичной модели (эта частичная модель может также содержать другие литералы, в зависимости от приложения). В этом случае распространение единиц выполняется на основе литералов частичной модели, а предложения единиц удаляются, если их литерал находится в модели. В приведенном выше примере предложение unitбудет добавлен к частичной модели; затем упрощение набора предложений будет продолжаться, как указано выше, с той разницей, что предложение unitтеперь удален из набора. Результирующий набор предложений эквивалентен исходному в предположении действительности литералов в частичной модели.
Сложность
Прямая реализация единичного распространения занимает время, квадратичное по отношению к общему размеру проверяемого набора, который определяется как сумма размеров всех предложений, где размер каждого предложения - это количество содержащихся в нем литералов.
Однако распространение единиц может выполняться за линейное время, сохраняя для каждой переменной список предложений, в которых содержится каждый литерал. Например, приведенный выше набор может быть представлен нумерацией каждого пункта следующим образом:
а затем сохраняя для каждой переменной список предложений, содержащих переменную или ее отрицание:
Эта простая структура данных может быть построена во времени линейно по размеру набора и позволяет очень легко находить все предложения, содержащие переменную. Единичное распространение литерала может быть эффективно выполнено путем сканирования только списка предложений, содержащих переменную литерала. Точнее, общее время выполнения распространения модуля для всех предложений модуля линейно зависит от размера набора предложений.
Смотрите также
Рекомендации
- Доулинг, Уильям Ф .; Gallier, Жан H. (1984), "Алгоритмы Linear времени для проверки выполнимости пропозициональных формул Horn", журнал логического программирования , 1 (3): 267-284, DOI : 10,1016 / 0743-1066 (84) 90014- 1 , Руководство по ремонту 0770156.
- Х. Чжан и М. Штикель (1996). Эффективный алгоритм для распространения единиц. В материалах Четвертого Международного симпозиума по искусственному интеллекту и математике .