График импликации - Implication graph
В математическая логика, граф импликации это кососимметричный ориентированный граф G = (V, E) составлен из множества вершин V и направленный набор кромок E. Каждая вершина в V представляет истинный статус Логический литерал, и каждое направленное ребро из вершины ты к вершине v представляет материальное значение "Если буквальный ты верно, то буквальный v также верно ". Графики импликации изначально использовались для анализа сложных Логические выражения.
Приложения
А 2-выполнимость экземпляр в конъюнктивная нормальная форма можно преобразовать в граф импликации, заменив каждый его дизъюнкции парой импликаций. Например, утверждение можно переписать как пару . Экземпляр является выполнимым тогда и только тогда, когда ни один литерал и его отрицание не принадлежат одному и тому же компонент сильной связности его графа импликации; эту характеристику можно использовать для решения случаев 2-выполнимости за линейное время.[1]
В CDCL СИДЕЛ -ольверы, единичное распространение может быть естественным образом ассоциирован с графом импликации, который захватывает все возможные способы получения всех подразумеваемых литералов из литералов решений,[2] который затем используется для изучения предложений.
Рекомендации
- ^ Аспвалл, Бенгт; Пласс, Майкл Ф.; Тарджан, Роберт Э. (1979). «Алгоритм линейного времени для проверки истинности определенных количественных булевых формул». Письма об обработке информации. 8 (3): 121–123. Дои:10.1016/0020-0190(79)90002-4.
- ^ Пол Бим; Генри Каутц; Ашиш Сабхарвал (2003). Понимание силы обучения по клаузулам (PDF). IJCAI. С. 1194–1201.