2-SAT

A pianist has to decide which hand plays each note. The rules are simple: a hand does not take notes wider than its stretch at once, and the hands do not cross: if two notes sound together, the lower one cannot be in the right hand while the upper one is in the left. Each rule talks about two notes at once: “this one or that one”, “if this one, then that one too”. This is the 2-SAT problem, and it is solved in a single traversal of a graph. Below are five real pieces, from a Bach prelude to an organ toccata, and for each note the hand the solution gave.

Bach’s Prelude in C major and Joplin’s “Maple Leaf Rag” are fine with hands that stretch an octave. Chopin’s Prelude in C minor needs a ninth, 14 semitones: at 13 there is a contradiction at 21 notes. On the sixth beat the right hand, according to the score, takes a chord from D♭3 to E♭4, exactly 14 semitones, while E♭1 sounds in the bass. “The Entertainer” requires a tenth. Bach’s organ toccata is too much for two hands even with a tenth: it needs an eleventh, 17 semitones. And that makes sense: the organist plays the toccata’s bass notes with the feet, on the pedals, which have a third staff of their own in the score.

The solution does not know on which staff a note is written, yet in the four piano pieces 93–99 per cent of the notes went to the hand of their own staff. The rest are places where the rules allow either hand, and the answer picks one of them.

The idea

A variable is a note; the value “true” is the right hand, “false” the left. A literal is a variable or its negation. A condition of two literals “a or b” says exactly the same as two implications: “if not a, then b” and “if not b, then a”. Draw a graph: the vertices are all 2n literals, the arrows two per condition. This is the implication graph: if a literal is true, everything that can be reached from it along the arrows is true.

A formula is unsatisfiable exactly when for some variable x one can get from x to ¬x along the arrows and back, that is, x and ¬x lie in one strongly connected component. Otherwise it is satisfiable, and the answer is: x is true if its component comes after the component of ¬x in topological order.

The rules for the hands are written like this. Notes a below b sound together, and the hands do not cross: “a left or b right”. If the gap between them is wider than the stretch, one hand cannot take them: “a right or b right” and “a left or b left”, that is, not both in one hand. Here is the graph of that chord from the Chopin prelude on which the contradiction rests: the “right” literals above, the “left” ones below. Click a literal, and everything that follows from it is filled in.

At 13 semitones from any literal the arrows lead to its negation: the whole graph is one component. At 14, “C4 right” implies exactly six literals, and together they give the distribution of the whole chord, as in the score: the five upper notes in the right hand, the bass E-flats in the left.

Why it is correct

The implication graph has a symmetry: an arrow a → b exists if and only if an arrow ¬b → ¬a exists, since both came from the same condition “¬a or b”. So paths are mirrored too: from a you can reach b exactly when from ¬b you can reach ¬a.

The components and their topological order come from a single traversal, Tarjan’s or Kosaraju’s, so the whole algorithm runs in O(n + m). In Tarjan’s algorithm components are numbered in reverse topological order: the first to close is the one from which there is no way out. So in code the rule reads: x is true if the number of its component is smaller than the number of the component of ¬x.

Three literals per condition change everything. 3-SAT is the first problem for which, in 1971, Stephen Cook proved NP-completeness, and no fast algorithm for it is known. The implication graph does not work: “a or b or c” does not reduce to arrows from one literal to one. Two hands and notes are on the boundary where the problem is still easy: a rule “no more than five notes in one hand” would talk about six notes at once and no longer fits this model.

Code

Literal 2i is note i in the right hand, 2i + 1 in the left, and the negation of a literal is x ^ 1. In the output notes are named with letters and octave numbers: C4 is middle C, Eb is E-flat. A MIDI file stores the key but not how each note is spelled, so the black keys are named according to the key of the piece. The condition “a or b” is a function that adds two arrows. Pairs of notes sounding together are enumerated over sorted starts: as soon as the next note starts after the end of the current one, there is no need to look further. Components are Tarjan without recursion. For each piece the program looks for the smallest stretch at which two hands suffice, and for two stretches where they do not, it writes out the chain of arrows that makes a note ask for both hands.

The Chopin chain can be read aloud. If middle C (C4 in the output) is in the right hand, then the E-flat above it (Eb4) is in the right too: the hands do not cross. Between that E-flat and D♭3 there are 14 semitones, more than the stretch, so the D-flat is in the left hand. The D-flat and the bass E♭1 cannot be taken by one hand either, so the bass is in the right. And the bass and the C certainly cannot be taken by one hand, so the C is in the left. The reverse chain is shorter: if the C is in the left, the bass below it is in the left too, but together they do not fit in a hand, so the C is in the right. In the toccata the pedal A2 does the same: it sounds under an A major chord from E4 to A5, an eleventh.

What it costs

The naive method, trying a variable as true, propagating the consequences and backtracking on a contradiction, is fast on random formulas. But it can be trapped: let k variables lead into the start of a long chain of implications whose end requires both w and ¬w. It tries each of the k variables as true, walks the whole chain, runs into the contradiction and backtracks, remembering nothing.

Search with propagation grows as a square: on two thousand variables it is 78 times slower than components in Python and 109 times slower in Go. Components pass each arrow once, however many traps there are.

Where it is easy to go wrong

• One arrow instead of two. The condition “a or b” is both ¬a → b and ¬b → a. Without the second arrow the symmetry the proof rests on disappears, and the answer may violate the condition.
• A one-literal condition. “a is required” is written as “a or a”: the arrow ¬a → a. Then ¬a cannot be true: a follows from it.
• The order of components. In Tarjan’s algorithm component numbers go in reverse topological order, in Kosaraju’s in forward order. The rule “true if the component is later” looks different in code, and mixing it up gives, on a satisfiable formula, an assignment that violates the conditions.
• Recursion. A recursive Tarjan will crash on a long chain of implications, as in the trap from the measurement. A traversal with its own stack will not.
• The model matters more than the algorithm. The rule “the hands do not cross” is broken in real music: in the toccata and in the rags the hands sometimes swap places. 2-SAT honestly answers the problem it was given.

Where it works

Timetables where each event has two possible times and some pairs of events cannot coincide. Map labels: a label to the left or right of its point, and two labels must not overlap; this is how the villages are labelled in the article on random walks. Splitting points into two clusters with the smallest sum of diameters: for each pair of thresholds this is 2-SAT. In large SAT solvers two-literal clauses are singled out and handled through the implication graph; they are the cheapest part of a formula.

History

Formulas of two-literal conditions were studied by Melven Krom in 1967, and they are sometimes called Krom formulas. In 1976 Shimon Even, Alon Itai and Adi Shamir arrived at 2-SAT from a timetabling problem and gave a polynomial algorithm. In 1979 Bengt Aspvall, Michael Plass and Robert Tarjan showed that one traversal over strongly connected components is enough; that is the algorithm in this article. And in 1991 Christos Papadimitriou gave an entirely different route, random flips of variables.

Problems

Notes and a hand’s stretch: find which hand plays each note, or prove that two hands are not enough. Among the tests are the same five pieces at different stretches.