Two literals make an arrow

A proof with one rule showed that resolution — combining two clauses that disagree about one variable into a clause that forgets it — refutes every unsatisfiable set of clauses. It also noted, in passing, that on clauses with only two literals the method never runs away: resolving two such clauses gives a clause with at most two literals, so there are only so many to derive.

That observation has a much sharper form. A clause of two literals is not really a disjunction at all. It is a pair of arrows, and a set of such clauses is a map of which literals force which. Satisfiability becomes a question about getting from one place on the map to another.

A clause is two implications #

Take the clause $p \vee q$. It is satisfied unless both $p$ and $q$ are false. So if $p$ is false, $q$ must be true, and if $q$ is false, $p$ must be true: the clause says exactly $\neg p \to q$, and it says exactly $\neg q \to p$. Both implications are the whole clause; neither adds anything the other lacks.

Draw a node for every literal — $p$, $\neg p$, $q$, $\neg q$ and so on — and for every clause draw its two arrows. Five clauses on four variables give eight nodes and ten arrows. The two arrows of a clause always come as mirror images: if $a \to b$ is drawn, so is $\neg b \to \neg a$, which is the contrapositive. The figure places each literal opposite its negation’s position so that this symmetry is visible.

An arrow is a promise about assignments: any assignment that satisfies the clauses and makes the tail true makes the head true. Chains of arrows compose. If a path of arrows leads from $r$ to $\neg r$, then $r$ cannot be true, because making it true would force it false. In the drawn set the path is short: $r \to s$ from the clause $\neg r \vee s$, and $s \to \neg r$ from the clause $\neg r \vee \neg s$.

If a second path leads back from $\neg r$ to $r$, then $r$ cannot be false either. Here it runs $\neg r \to \neg p \to q \to r$, through three more clauses. With both paths present, no value of $r$ survives, and so no assignment satisfies the set.

A cycle that makes something impossible is a familiar shape. The majority that goes in a circle finds three voters whose pairwise majorities prefer A to B, B to C and C to A, so that no ranking agrees with every majority. Here the cycle runs through a literal and its own negation, so no truth value agrees with every clause; in both cases a loop of individually reasonable demands leaves nothing that meets them all.

The paths are the refutation #

That argument about arrows is a resolution proof in disguise, and it can be written out step by step.

Follow a path and resolve the clauses its arrows came from, in order. The clause behind $r \to s$ is $\neg r \vee s$, and the clause behind $s \to \neg r$ is $\neg r \vee \neg s$; they clash on $s$, and resolving them leaves $\neg r \vee \neg r$, which is simply $\neg r$. In general a path from $x$ to $y$ resolves, arrow by arrow, into the clause $\neg x \vee y$ — the single implication $x \to y$ that the whole path amounts to — because each resolution step cancels the literal the path passes through.

The second path gives $r$: its clauses $\neg p \vee r$ and $p \vee q$ resolve on $p$ into $q \vee r$, and that resolves with $\neg q \vee r$ on $q$ into $r$. The unit clauses $\neg r$ and $r$ resolve into the empty clause. Every step in the figure was checked against the rule rather than drawn.

The correspondence runs the other way too. Every two-literal clause that resolution can derive from the set, $a \vee b$, corresponds to a path from $\neg a$ to $b$ in the graph, since derivations and paths are built by the same composition. Resolution on two-literal clauses is exactly the computation of which literals reach which. A refutation is a pair of paths, one from a literal to its negation and one back.

Three ways to decide the same sets #

The claim that a set is unsatisfiable exactly when some variable and its negation reach each other can be checked on every set of its kind that fits on three variables. There are twelve possible two-literal clauses on three variables, so 4,095 non-empty sets of them, the same family the previous essay swept with truth tables and resolution. The arrow method is a third, independent verdict, and all three agree on every set: 1,699 unsatisfiable, 2,396 not.

The work columns in the note are honest about scale. On three variables, resolution derived 29,347 clauses in total across all the sets and the arrow method examined 49,152 arrows, twice the number of clauses it was given. On instances this small the arrows are not cheaper; everything is cheap. The difference is how the two grow. Resolution’s closure can hold a number of clauses proportional to the square of the number of variables, and computing it naively compares clauses in pairs. The arrow method touches each arrow a fixed number of times, whatever the size.

Storing the direct steps, not every consequence #

Why the arrows win as instances grow can be seen on the simplest set there is: a chain of implications $x_1 \to x_2 \to \cdots \to x_{42}$, written as the 41 clauses $\neg x_i \vee x_{i+1}$. Resolution, run until nothing new appears, derives every consequence: $\neg x_i \vee x_j$ for every pair with $i < j$. That is $42 \cdot 41 / 2 = 861$ clauses, of which all but the original 41 are new, and a longer chain makes the count grow with the square of its length.

The graph stores 82 arrows — each clause and its mirror — and never writes down a consequence. It answers “does $x_3$ force $x_{40}$?” by walking from one to the other when asked. Resolution computes the transitive closure of the arrows; the component algorithm only needs to know which nodes lie on common cycles, and it finds that out without materialising a single derived clause.

That is a general trade between proof and procedure. A refutation is a finite object that can be checked, and it lists everything it uses. A decision procedure only has to be right, and it can afford to leave most consequences unstated.

Components, found in one pass #

Asking whether $x$ reaches $\neg x$ and $\neg x$ reaches $x$ for every variable separately would repeat work. The efficient version groups the literals into strongly connected components: maximal sets in which every literal reaches every other. A variable is doomed exactly when $x$ and $\neg x$ fall in the same component.

Robert Tarjan’s algorithm of 1972 finds all the components of a directed graph in a single depth-first pass, touching each node and each arrow a bounded number of times. Aspvall, Plass and Tarjan applied it to two-literal clauses in 1979, giving a decision procedure whose running time is proportional to the number of clauses. Krom had shown in 1967 that such clauses can be decided efficiently by resolution; the graph made it linear.

Linear time is the best any procedure could manage, since it has to read the clauses. For clauses of three literals no procedure is known that is even polynomial, and none can be unless every problem whose solutions can be checked quickly can also be solved quickly. Two literals and three literals sit on opposite sides of the most famous open boundary in computing.

Reading an assignment off the components #

When no variable shares a component with its negation, the set is satisfiable, and the components do more than say so: their order produces a satisfying assignment.

Tarjan’s algorithm finishes components in a useful order: a component is finished only after every component it can reach. Make each variable true when its positive literal’s component was finished before its negation’s. In the drawn set, $p$, $r$ and $s$ form one component, their negations another, and $q$ and $\neg q$ sit alone; every variable comes out true, and every clause is satisfied.

The reason it always works fits in a paragraph. Suppose some arrow $a \to b$ ran from a true literal to a false one. Its mirror $\neg b \to \neg a$ also exists. Since $b$ is false, $\neg b$’s component finished before $b$’s; since $a$ is true, $a$’s finished before $\neg a$’s. But an arrow from one component to another means the second finished first, so $b$ finished no later than $a$, and $\neg a$ no later than $\neg b$. Chaining these gives $\neg a$ before $\neg b$ before $b$ before $a$ before $\neg a$, which is impossible. So no arrow leaves a true literal for a false one, and a clause $a \vee b$, whose arrow $\neg a \to b$ would otherwise run from true to false, is always satisfied.

Colouring a map with two colours #

Two-literal clauses describe more problems than they appear to. Colour the corners of a network with two colours so that the two ends of every link differ. Give each corner a variable, true for one colour and false for the other; a link between $u$ and $v$ becomes the two clauses $u \vee v$ and $\neg u \vee \neg v$, saying the ends are not both false and not both true.

The arrows of those clauses say that each link flips the colour: $\neg u \to v$ and $u \to \neg v$. A corner reaches its own opposite colour exactly when some closed walk crosses an odd number of links, so the network can be two-coloured exactly when it has no odd cycle — the classical criterion, recovered from the components. Counting the colourings asks the harder question of how many colourings there are, and with three colours even deciding whether one exists needs clauses of three literals: every corner must take at least one of three colours.

For regions of a flat map the same reasoning applies to the network of neighbouring regions: two colours suffice exactly when no ring of neighbours has odd length, while the question of whether four always suffice took the computer-assisted case analysis of four colours and a proof nobody can read.

The seven bridges turned a question about walking every link into counting at the corners. Here the traffic runs the other way: a question about assignments is turned into walking the links.

Random sets and a sudden change #

Fast decisions make large experiments possible. Choose clauses at random — two different variables, each negated or not by a coin — and count how many of 120 random sets can be satisfied at each ratio of clauses to variables. Below one clause per variable almost every set is satisfiable. Above one, the share falls, and it falls faster the more variables there are: at 1.2 clauses per variable, 88 per cent of the sets on 50 variables survive, 68 per cent on 200, and 42 per cent on 800.

The limit is a theorem, proved independently by Chvátal and Reed and by Goerdt in the early 1990s: as the number of variables grows, the probability that a random set is satisfiable tends to 1 for every ratio below 1 and to 0 for every ratio above. The picture is the same kind of transition as the random networks of sharp or merely a threshold, and for the same kind of reason. Unsatisfiability needs a long chain of arrows from some literal to its negation and back, and chains of that kind become likely around the point where a random graph of arrows starts to form one giant tangle of mutually reachable nodes — roughly when the average node has one arrow leaving it, which is one clause per variable.

The second-moment arguments of finding a threshold with two moments are the tool for proofs like this one: showing that the expected number of contradictory chains is large is not enough, and the variance has to be controlled as well.

Where the arrows stop #

Three literals do not make arrows. A clause $p \vee q \vee r$ says that if $p$ and $q$ are both false then $r$ is true — an implication with two conditions, which is an edge joining three nodes rather than an arrow joining two. Resolving two such clauses can produce four literals, and the derived clauses grow. The pigeonhole clauses of more things than boxes have a clause saying each pigeon sits in some hole, with as many literals as there are holes, and that is where the next essay’s difficulty lives.

Deciding is not optimising. The arrows say in linear time whether every clause can be satisfied. Asking for an assignment satisfying as many clauses as possible, when not all can be, is hard even for two literals — no efficient method is known, and none is expected.

And two literals cannot say everything. A set of two-literal clauses describes a special kind of constraint, closed under a particular way of combining assignments. By one connective is enough, any truth function can be written as clauses, but not as clauses of two literals: “an odd number of $p$, $q$ and $r$ are true” needs longer ones.

Eight nodes cannot show linear time #

Every graph drawn has four variables. The linear-time claim is about growth, and a figure on eight nodes cannot show growth. The sweep over 4,095 sets establishes the three-way agreement on three variables and says nothing about time.

The random sets are samples. A share of 0.42 from 120 sets carries an uncertainty of several per cent, which is why the curve for 50 variables is ragged. The theorem is about limits, and the curves only illustrate the trend towards them.

And the component order is one valid order. Tarjan’s algorithm can finish components in different orders depending on where it starts, and each gives a satisfying assignment, possibly a different one. The figure shows the assignment for the order the algorithm happened to take.

Still open: where random three-literal clauses flip #

Random sets of three-literal clauses also flip from satisfiable to unsatisfiable, and computer experiments put the change at about 4.27 clauses per variable. That value has never been proved. Friedgut showed in 1999 that the change is sharp, but not that it happens at a fixed ratio rather than drifting with the number of variables; the best proved bounds say it lies somewhere between about 3.52 and 4.49. For clauses of sufficiently many literals, Ding, Sly and Sun proved in 2015 that the threshold exists and located it exactly, confirming a prediction from statistical physics. For three literals — the smallest case where the arrows no longer work — the question remains open.

Change the representation before changing the method #

Resolution on two-literal clauses is complete and efficient already, but it looks like bookkeeping on disjunctions. Redrawn as arrows, the same computation is reachability in a graph, the refutation is a pair of paths, the decision is a single pass that finds components, and a satisfying assignment falls out of the order the components were found in.

When a proof system restricted to a fragment becomes fast, look for the structure the fragment has. Here it is a graph, and the graph turns a logical question into one about walking — which is why two literals are easy, and why three, which do not make arrows, are not.