algorithm2-satisfiabilitykosaraju-algorithm

2-SAT variable values

2-SAT problem, finding value for variables

I'm using this solution for finding satisfiability for given formula. (by checking SCC). Is there any efficient way (efficient means not worse than polynomial time in my case) how to find value for each variable if formula is satisfiable?

It doesn't have to be in C++, I'm just using the same algorithm.

Solution

  • As described in the linked answer, you can turn a 2-SAT problem into an implication graph, because (x|y) <=> (~x => y) & (~y => x)

    To make a satisfying assignment, we need to choose, for every variable x, either x or ~x such that:

    1. If we choose a term x, then we also choose everything that x implies in the transitive closure of the implication graph, and similarly for ~x; and
    2. If we choose x, then we also choose the negation of everything that implies ~x in the transitive closure of the implication graph.

    Because of the way we constructed the implication graph, rule (2) is already covered by rule (1). If (a => ~x) is in the graph, then (x => ~a) is also in the graph. Also if (a => b) & (b => ~x), then we have (x => ~b) & (~b => ~a).

    So really there is only rule (1). This leads to a linear time algorithm that is similar to a topological sort.

    If we were to collapse every SCC in the graph into a single vertex, the result would be acyclic. There must be at least one SCC in the graph, therefore, that has no outgoing implications.

    So:

    1. Initialize the selected assignment to empty;
    2. Select an SCC that has no outgoing implications. If it doesn't contradict anything in the current assignment, then add all its terms to the current assignment. Otherwise, add the negation of all of its terms, and add at least one contradiction for every SCC that directly implies it.
    3. Remove the selected SCC from the graph, and go back to (2) until the graph is empty.

    Repeat until the graph is empty. The process will always terminate, since removing SCCs doesn't introduce cycles.

    Step (2) ensures that, before we remove an SCC from the graph, the current assignment establishes the truth or falsehood of everything that had an implication to it.

    If the problem instance was satisfiable, then you'll be left with a satisfying assignment for every variable that is mentioned in the problem.