Как описано в связанном ответе, вы можете превратить проблему 2-SAT в граф импликации, потому что (x | y) <=> (~ x => y) & (~ y => x)
Чтобы выполнить удовлетворительное назначение, нам нужно выбрать для каждой переменной x : x или ~ x , чтобы:
- Если мы выберем термин x , то мы также выберем все, что x подразумевает в транзитивном замыкании графа импликации, и аналогично для ~ х ;и
- Если мы выберем x , то мы также выберем отрицание всего, что подразумевает ~ x в транзитивном замыкании графа импликации.
Из-за способа построения графа импликации правило (2) уже охватывается правилом (1).Если (a => ~ x) находится на графике, то (x => ~ a) также находится на графике.Также, если (a => b) & (b => ~ x) , то имеем (x => ~ b) & (~ b => ~ a) .
Так что на самом деле есть только правило (1).Это приводит к линейному алгоритму времени, который похож на топологическую сортировку.
Если бы мы свернули каждый SCC в графе в одну вершину, результат был бы ациклическим.Поэтому на графике должен быть хотя бы один SCC, который не имеет исходящих последствий.
Итак:
- Инициализируйте выбранное назначение пустым;
- ВыбратьSCC, который не имеет исходящих последствий.Если это не противоречит чему-либо в текущем назначении, то добавьте все его термины в текущее назначение.В противном случае добавьте отрицание всех его членов и добавьте хотя бы одно противоречие для каждого SCC, который непосредственно подразумевает это.
- Удалите выбранный SCC из графика и возвращайтесь к (2), пока график не станетпусто.
Повторяйте, пока график не станет пустым.Процесс всегда завершается, так как удаление SCC не вводит циклы.
Шаг (2) гарантирует, что, прежде чем мы удалим SCC из графика, текущее назначение устанавливает правдивость или ложность всего, что имелоследствие этого.
Если экземпляр задачи был выполнимым, то у вас останется удовлетворительное присваивание для каждой переменной, упомянутой в проблеме.