2-SAT

Пианисту нужно решить, какой рукой играть каждую ноту. Правила простые: рука не берёт разом ноты шире своей растяжки, и руки не перекрещиваются — если две ноты звучат вместе, нижняя не может быть у правой руки, когда верхняя у левой. Каждое правило говорит о двух нотах сразу: «эта или та», «если эта, то и та». Это задача 2-SAT, и она решается за один обход графа. Ниже пять настоящих пьес — от прелюдии Баха до органной токкаты, — и для каждой ноты рука, которую дало решение.

Прелюдии Баха до мажор и «Рэгу кленового листа» Джоплина хватает рук с растяжкой в октаву. Прелюдии Шопена до минор нужна нона, 14 полутонов: при 13 противоречие у 21 ноты. На шестой доле правая рука по нотам берёт аккорд от ре-бемоля малой октавы до ми-бемоля первой — ровно 14 полутонов, а в басу звучит ми-бемоль контроктавы. «Конферансье» требует децимы. Органной токкате Баха двух рук мало даже с децимой: нужна ундецима, 17 полутонов. Это и понятно: басы токкаты органист играет ногами, на педали, — у неё в нотах свой, третий стан.

Решение не знает, на каком стане записана нота, но в четырёх фортепианных пьесах 93–99 процентов нот попали в руку своего стана. Остальные — места, где правила разрешают обе руки, и ответ выбирает одну из них.

Идея

Переменная — нота; значение «истина» — правая рука, «ложь» — левая. Литерал — переменная или её отрицание. Условие из двух литералов «a или b» говорит ровно то же, что две импликации: «если не a, то b» и «если не b, то a». Нарисуем граф: вершины — все 2n литералов, стрелки — по две на каждое условие. Это граф следствий: если литерал истинен, истинно всё, до чего от него можно дойти по стрелкам.

Формула невыполнима ровно тогда, когда для какой-то переменной x из x по стрелкам можно дойти до ¬x и обратно — то есть x и ¬x лежат в одной компоненте сильной связности. Иначе выполнима, и ответ таков: x истинна, если её компонента идёт позже компоненты ¬x в топологическом порядке.

Правила для рук записываются так. Ноты a ниже b звучат вместе — руки не перекрещиваются: «a левой или b правой». Если между ними больше растяжки, одной рукой их не взять: «a правой или b правой» и «a левой или b левой» — то есть не обе у одной руки. Вот граф того аккорда из прелюдии Шопена, на котором держится противоречие: сверху литералы «правой», снизу «левой». Нажмите на литерал — закрасится всё, что из него следует.

При 13 полутонах из любого литерала по стрелкам доходим до его отрицания: весь граф — одна компонента. При 14 из «C4 правой» следуют ровно шесть литералов, и вместе они дают раздачу всего аккорда, как в нотах: пять верхних нот у правой руки, басовые ми-бемоли у левой.

Почему это верно

У графа следствий есть симметрия: стрелка a → b есть тогда и только тогда, когда есть стрелка ¬b → ¬a, ведь обе пришли из одного условия «¬a или b». Поэтому и пути отражаются: из a можно дойти до b ровно тогда, когда из ¬b можно дойти до ¬a.

Компоненты и их топологический порядок даёт один обход — Тарьяна или Косараю, — поэтому весь алгоритм работает за O(n + m). У Тарьяна компоненты получают номера в обратном топологическом порядке: первой закрывается та, из которой никуда не выйти. Поэтому в коде правило читается так: x истинна, если номер её компоненты меньше номера компоненты ¬x.

Три литерала в условии меняют всё. Задача 3-SAT — первая задача, для которой в 1971 году Стивен Кук доказал NP-полноту, и быстрого алгоритма для неё не знают. Граф следствий не работает: «a или b или c» не сводится к стрелкам из одного литерала в один. Две руки и ноты — граница, где задача ещё лёгкая: правило «не больше пяти нот у одной руки» говорило бы о шести нотах сразу и в эту модель уже не влезает.

Код

Литерал 2i — нота i у правой руки, 2i + 1 — у левой, отрицание литерала — x ^ 1. В выводе ноты названы латинскими буквами: C — до, D — ре, E — ми и так далее, Eb — ми-бемоль, C4 — до первой октавы. MIDI-файл хранит тональность, но не то, как записана каждая нота, поэтому чёрные клавиши названы по тональности пьесы. Условие «a или b» — функция, которая кладёт две стрелки. Пары нот, звучащих вместе, перебираются по отсортированным началам: как только следующая нота начинается после конца текущей, дальше смотреть не нужно. Компоненты — Тарьян без рекурсии. Для каждой пьесы программа ищет наименьшую растяжку, при которой двух рук хватает, а для двух растяжек, где не хватает, выписывает цепочку стрелок, из-за которой нота просится в обе руки.

Цепочку у Шопена можно прочитать вслух. Если до первой октавы (в выводе C4) у правой руки, то и ми-бемоль над ним (Eb4) у правой — руки не перекрещиваются. Между ми-бемолем и ре-бемолем малой октавы (Db3) 14 полутонов, больше растяжки, — значит, ре-бемоль у левой. Ре-бемоль и басовое ми-бемоль контроктавы (Eb1) одной рукой тоже не взять — бас у правой. А бас и до тем более не взять одной рукой — до у левой. Обратная цепочка короче: если до у левой, то и бас под ним у левой, но вместе они в руку не помещаются — до у правой. В токкате то же делает педальное ля большой октавы (A2): оно звучит под аккордом ля мажор от ми первой октавы до ля второй — это ундецима.

Сколько это стоит

Наивный способ — попробовать переменную истинной, распространить следствия и откатиться, если пришли к противоречию, — на случайных формулах работает быстро. Но его можно поймать: пусть k переменных ведут в начало длинной цепочки следствий, конец которой требует и w, и ¬w. Каждую из k переменных он пробует истинной, проходит всю цепочку, упирается в противоречие и откатывается, ничего не запомнив.

Перебор с распространением растёт как квадрат: на двух тысячах переменных он медленнее компонент в 78 раз на Python и в 109 раз на Go. Компоненты проходят каждую стрелку один раз, сколько бы ни было ловушек.

Где легко ошибиться

• Одна стрелка вместо двух. Условие «a или b» — это и ¬a → b, и ¬b → a. Без второй стрелки пропадает симметрия, на которой держится доказательство, и ответ может нарушить условие.
• Условие из одного литерала. «a обязательно» записывается как «a или a»: стрелка ¬a → a. Тогда ¬a не может быть истинным: из него следует a.
• Порядок компонент. У Тарьяна номера компонент идут в обратном топологическом порядке, у Косараю — в прямом. Правило «истинно, если компонента позже» в коде выглядит по-разному, и перепутать его — значит получить набор, нарушающий условия, на выполнимой формуле.
• Рекурсия. Рекурсивный Тарьян упадёт на длинной цепочке следствий — как в ловушке из замера. Обход со своим стеком — нет.
• Модель важнее алгоритма. Правило «руки не перекрещиваются» в настоящей музыке нарушают — в токкате и в рэгах руки иногда меняются местами. 2-SAT честно отвечает на ту задачу, которую ему дали.

Где работает

Расписания, где у каждого события два возможных времени, а некоторые пары событий не могут совпадать. Подписи на картах: подпись слева или справа от точки, и две подписи не должны пересекаться — так подписаны сёла в статье о случайных блужданиях. Разбиение точек на два кластера, при котором сумма диаметров наименьшая: для каждой пары порогов это 2-SAT. В больших решателях SAT условия из двух литералов выделяют и обрабатывают через граф следствий — это самая дешёвая часть формулы.

История

Формулы из условий по два литерала изучал Мелвен Кром в 1967 году — их иногда называют формулами Крома. Шимон Ивен, Алон Итаи и Ади Шамир в 1976 году пришли к 2-SAT из задачи о расписаниях и дали полиномиальный алгоритм. В 1979 году Бенгт Аспвалль, Майкл Пласс и Роберт Тарьян показали, что хватает одного обхода по компонентам сильной связности, — это алгоритм из статьи. А в 1991 году Христос Пападимитриу дал совсем другой путь — случайные перевороты переменных.

Задачи

Ноты и растяжка руки — найти, какой рукой играть каждую ноту, или доказать, что двух рук мало. Среди тестов — те же пять пьес при разных растяжках.