Алгоритм Horn SAT с использованием графиков

Question

Для некоторых ограниченных классов логических формул проблема выполнимости может быть эффективно решена за полиномиальное время или даже линейно. Одним из таких классов является класс формул Хорна, которые состоят только из предложений Хорна с не более чем одним положительным литералом. Я слышал, что можно решить Horn SAT за линейное время с использованием графиков, но не нашел реализации такого решения. Теперь мне действительно интересно, возможно ли это, и если да, то как будет выглядеть алгоритм?

Answer 1

Если вы знакомы с формулами Дэвиса – Патнэма – Логеманна – Лавленда, предложения Хорна - это класс формул, которые могут быть решены с использованием одного раунда распространения единиц без возврата.

В терминах графа мы делаем очевидную вещь и создаем двудольный граф с переменными с одной стороны, предложениями с другой и ребрами, чтобы представить переменную, появляющуюся в предложении как отрицательный литерал. У нас также есть рабочая очередь предложений, состоящая из одного положительного литерала. Пока рабочая очередь не пуста, вытяните любой элемент, определите узел, соответствующий переменной, и удалите его и его соседей. Для каждой вершины предложения, которая теперь имеет нулевую степень, происходит одно из двух. Если это предложение имеет положительный литерал, мы добавляем его в очередь работ. В противном случае мы доказали, что формула невыполнима. Если мы дойдем до конца рабочей очереди, не найдя такого предложения, то формула выполнима, и одно удовлетворительное назначение - установить для всех переменных, которые вошли в рабочую очередь, значение true, а для всех остальных - значение false.