График последствий

Граф импликации, представляющий 2-выполнимости экземпляр $\scriptscriptstyle (x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \quad \scriptscriptstyle (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).$

В математической логике и теории графов импликационный граф — это кососимметричный ориентированный граф G = ( V , E ), состоящий из вершин множества V ребер E. и направленного множества Каждая вершина в V представляет статус истинности логического литерала , а каждое направленное ребро от вершины u до вершины v представляет собой материальную импликацию : «Если литерал u истинен, то литерал v также истинен». Графы импликаций изначально использовались для анализа сложных логических выражений .

Приложения

Экземпляр 2-выполнимости в конъюнктивной нормальной форме можно преобразовать в граф импликаций, заменив каждую из его дизъюнкций парой импликаций. Например, заявление $(x_{0}\lor x_{1})$ можно переписать в виде пары $(\neg x_{0}\rightarrow x_{1}),(\neg x_{1}\rightarrow x_{0})$. Экземпляр является выполнимым тогда и только тогда, когда ни один литерал и его отрицание не принадлежат одному и тому же сильно связному компоненту его графа импликаций; эту характеристику можно использовать для решения случаев 2-выполнимости за линейное время .

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