2-SAT значения переменной

Question

Задача 2-SAT, поиск значения для переменных

Я использую это решение для нахождения удовлетворенности для данной формулы. (проверяя ГТК). Есть ли эффективный способ (эффективный означает не хуже, чем полиномиальное время в моем случае), как найти значение для каждой переменной, если формула выполнима?

Это не обязательно должно быть в C++, я просто использую тот же алгоритм.

Answer 1

Как описано в связанном ответе, вы можете превратить проблему 2-SAT в граф импликации, потому что (x|y) <=> (~x => y) & (~y => x)

Чтобы выполнить удовлетворительное присваивание, нам нужно выбрать для каждой переменной x либо x, либо ~ x так, чтобы:

1. Если мы выберем термин x, то мы также выберем все, что x подразумевает в транзитивном замыкании графа импликации, и аналогично для ~ x; а также
2. Если мы выбираем x, то мы также выбираем отрицание всего, что подразумевает ~ x в транзитивном замыкании графа импликации.

Из-за способа построения графа импликации правило (2) уже охватывается правилом (1). Если (a => ~x) находится в графе, то (x => ~a) также находится в графе. Также, если (a => b) & (b => ~ x), то мы имеем (x => ~ b) & (~ b => ~ a).

Так что на самом деле есть только правило (1). Это приводит к линейному алгоритму времени, похожему на топологическую сортировку.

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

Так:

1. Инициализировать выбранное назначение как пустое;
2. Выберите SCC, который не имеет исходящих последствий. Если это не противоречит чему-либо в текущем назначении, то добавьте все его термины в текущее назначение. В противном случае добавьте отрицание всех его терминов и добавьте хотя бы одно противоречие для каждого SCC, которое непосредственно подразумевает это.
3. Удалите выбранный SCC из графика и возвращайтесь к (2), пока график не станет пустым.

Повторяйте, пока график не станет пустым. Процесс всегда завершается, так как удаление SCC не приводит к циклам.

Шаг (2) гарантирует, что, прежде чем мы удалим SCC из графа, текущее назначение устанавливает правду или ложь всего, что имело к этому отношение.

Если экземпляр задачи был выполнимым, то у вас останется удовлетворительное присваивание для каждой переменной, упомянутой в проблеме.