2-SAT

Some planning problems are a list of yes-or-no questions with rules between them. When each rule names at most two conditions, the strongly connected groups of one graph decide whether all the rules can hold, and give the answers if they can. This is 2-SAT.

Rules with two conditions

There are n questions x₁, …, xₙ, each answered yes (True) or no (False). A condition is either xᵢ (“question i is yes”) or its opposite ¬xᵢ (“question i is no”); the sign ¬ is read “not”. A rule is “a or b” for two conditions a and b: at least one of them must hold. The task is to answer every question so that every rule holds, or to say that no set of answers does.

Many kinds of rule fit this shape:

• “x must be yes” is (x or x).
• “not both x and y” is (¬x or ¬y).
• “if x then y” is (¬x or y).
• “x and y are answered the same” is two rules: (¬x or y) and (x or ¬y).

Example: each of n trains runs on the morning or the evening timetable, and some pairs of trains cannot both run in the same slot. Trying every set of answers means 2ⁿ sets (n twos multiplied together): over a million for n = 20, far too many for n = 100.

The implication graph

The rule (a or b) says two things. If a is false, b must hold. If b is false, a must hold. Write “if x holds, y must hold” as an edge x → y. Then each rule gives two edges:

The implication graph has 2n vertices, one for each condition, and 2 edges per rule. A path x → … → y means: if x holds, then y must hold too, by following the rules one at a time. The graph has a useful mirror shape: the two edges of each rule mirror each other, so there is an edge x → y exactly when there is an edge ¬y → ¬x, and the same holds for paths. The figure puts each condition opposite its negation, so each edge has its mirror edge on the opposite side.

def node(lit):                 # x_k is 2(k-1), not x_k is 2(k-1) + 1
    return 2 * (lit - 1) if lit > 0 else 2 * (-lit - 1) + 1

adj = [[] for _ in range(2 * n)]
for a, b in rules:
    x, y = node(a), node(b)
    adj[x ^ 1].append(y)       # not a -> b
    adj[y ^ 1].append(x)       # not b -> a

Numbering x_k as 2(k − 1) and ¬x_k as the next number makes the opposite of vertex x simply x ^ 1, which flips the lowest bit (BITS-2).

When there is no answer

If x and ¬x are in one group, there are paths x → … → ¬x and ¬x → … → x. Answering yes forces x to be false, and answering no forces it to be true. Neither works, so there is no answer. The figure’s second variant shows this, with a and ¬a marked red: the rules are broken whatever you choose.

If no question has both in one group, the next section builds a set of answers that keeps every rule, which proves the other direction.

Choosing the answers

Number the groups in topological order (lesson 1): every edge goes from a group to the same group or a later one. For each question, make true the condition whose group comes later:

Why every rule holds. Take a rule (a or b), and suppose both a and b came out false. Then the group of ¬a comes after the group of a, and the group of ¬b after the group of b. The rule gives the edge ¬a → b, so group(b) is at or after group(¬a); and it gives ¬b → a, so group(a) is at or after group(¬b). Putting the four facts in a row:

That says group(a) comes before itself, which is impossible. So at least one of a and b is true, for every rule.

With Tarjan’s method the groups come out in reverse topological order (lesson 2), so a smaller Tarjan number means later: answer yes when comp[x] < comp[x ^ 1]. With Kosaraju’s method the numbers are already in topological order: yes when comp[x] > comp[x ^ 1]. Getting this the wrong way round gives answers that break rules.

Cost. 2n vertices and 2m edges for m rules, and one search for groups: O(n + m). The search must not use recursion: a chain of rules makes a path in the implication graph as long as the whole graph. Now try CONN-P4, Yes-or-no rules.

Rules of three conditions are much harder

With rules of three conditions, such as (a or b or c), the problem is called 3-SAT, and no method is known that is much faster than trying a large share of the 2ⁿ answers. 3-SAT is NP-complete: HARD-1 explains what that means, and why a fast method for it would give fast methods for thousands of other problems. The step from two to three conditions is the step from one rule’s “if this then that” to a real choice: (a or b or c) does not force anything when one condition is false.

• Uses of 2-SAT. Placing labels on a map (each label above or below its point, no two overlapping), choosing one of two slots for each task with clashes, and the “teams” of GRPH-6 (x and y on different teams is (x or y) and (¬x or ¬y)).
• Counting answers. Finding one answer is fast, but counting how many answers 2-SAT rules have is as hard as the hardest counting problems. The groups give one answer, not all of them.