Задача булевой выполнимости (SAT) является одной из самых основополагающих задач в информатике и математике. Несмотря на свою сложность, она лежит в основе множества прикладных областей, охватывающих разные направления от проверки микропроцессоров до оптимизации маршрутов и криптографии. В недавней статье “SAT Solver Etudes I” Филипп Закер рассматривает методы решения таких задач с использованием языка Python, предоставляя ценный обзор мощных инструментов для работы с разными логическими задачами. Для полного понимания важно осознать, какие математические задачи негласно присутствуют в нашей повседневной жизни и как они связаны с SAT. Рассмотрим несколько примеров:  1) Логистическая оптимизация: Планирование маршрутов доставки, распределение ресурсов, составление расписаний – все эти задачи сводятся к поиску оптимального решения среди множества возможных вариантов, что напрямую связано с принципами SAT.

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

3) Искусственный интеллект: Многие алгоритмы машинного обучения, такие как автоматическое доказательство теорем или распознавание образов, используют SAT-технологии для поиска оптимальных решений в сложных пространствах данных.

Таким образом, SAT, будучи фундаментальной задачей, играет важную роль в различных областях нашей жизни, предоставляя мощные инструменты для решения сложных логических задач. Среди них выделяются:

• Прежде всего упомянем криптографический алгоритм RSA, которые используется для обеспечения безопасности банковских транзакций, а так же для создания безопасного соединения. Алгоритм RSA может быть «взломан» с помощью SAT.
• Многие рекомендательные системы (например, в составе Netflix) используют алгоритм разложения булевых матриц для рекомендации контента. Оптимальное разложение таких матриц может быть найдено с помощью SAT.
• Задача оптимального распределения задач по процессорам может быть решена с помощью SAT. Большое число задач планирования сводится к SAT, например, open shop scheduling, где задачи (jobs) должны пройти определенные стадии (выполненными определенными рабочими) и необходимо минимизировать общую продолжительность обработки всех задач.
• NASA проверяет спецификации своего программного обеспечения и моделей своего технического обеспечения с помощью методов model checking, напрямую связанного с SAT.
• Популярный метод кластеризации k-means (метод к-средних) может быть решен с помощью SAT.
• Большинство интересных задач связанных с графами (например, в социальных сетях, граф — это отношение дружбы между пользователями) — поиск наибольшего сообщества, где каждый дружит с каждым, поиск самого длинного пути и многие другие задачи на графах могут быть решены с помощью SAT. Задача из жизни московской области (и не только): составить расписание мусоровозов таким образом, чтобы они объехали все пункты сбора мусора по одному разу за минимальное время. Большое число задач в логистике сводится к задаче SAT.
• Даже задача о ранце может быть решена с помощью SAT. Задача состоит в том, чтобы имея ранец фиксированного размера, набрать в него предметов наибольшей ценности (зная размеры всех предметов заранее).
• Многие видео игры могут быть решены с помощью SAT (и даже Марио!) Так же пазл Судоку и, внимание, Сапер могут быть решены с помощью SAT!
• Задачи о сериализации истории транзакций в базах данных может быть решена с помощью SAT.

Визуализация задач, решаемых с помощью SAT (due to Bart Selman, взято отсюда)

Что значит «могут быть решены» и при чем тут NP

Упрощенно говоря, если у нас есть эффективное решение задачи SAT, то мы можем эффективно решать все указанные задачи. Что конкретно подразумевается под эффективностью зависит от конкретной задачи, но здесь будем считать, что время работы является приемлемым для пользователя (для составления расписания школы на семестр, мы можем посвятить пару дней вычислениям, а для метода кластеризации, мы бы хотели получить результат в интерактивном режиме). А для многих из указанных выше задач верно и обратное, если мы умеем эффективно решать их, то мы умеет эффективно решать SAT (это и называется NP-полнотой — данное определение неформально, но достаточно для общего понимания).

Все эти задачи лежат в классе NP — позднее мы опишем класс детальнее, сейчас же нам стоит отметить, что, если известно эффективное решение задачи SAT, то мы можем эффективно решать любую задачу в классе NP. Иначе говоря, SAT — это задача представитель класса, она является «сложнейшей» в своем классе и позволяет решить все другие задачи в NP.

История SAT и NP-полноты

NP-полнота

Теория вычислительной сложности, в которой языки и функции выделяют в разные классы по количеству времени и памяти необходимые для их вычислений, родилась из теории вычислимости (т.е. работ 30ых годов Гёделя, Чёрча и Тьюринга), когда Хартманис, Штернc, Левис (1965) предложили одну из первых подобных классификаций функций (оригинальные работы: тут и тут).

Концепция NP-полноты развивалась в 1960х-1970х годах независимо в СССР и CША (Эдмондс, Левин, Яблонский et al.). В 1971 году Стивен Кук сформулировал гипотезу о P vs. NP. Теорему о том, что SAT является «универсальной задачей» для класса NP и позволяет решить любую задачу в этом классе (NP-полнота) независимо доказали Леонид Левин (1973) и Стивен Кук, и называется теоремой Левина-Кука. В 1982ом Кук получит за эту работу премию Тьюринга.

В 1972ом Карп публикует Reducibility among combinatorial problems, список показывающий, что SAT далеко не единственная интересная задача в NP и огромное количество задач лежит в NP и эквивалентно SAT. В 1985ом Карп получит за эту работу премию Тьюринга.

В 1974ом Фагин покажет, что NP тесно связан с классической логикой, а именно, что NP эквивалентен экзистенциальным логическим структурам второго порядка (теорема Фагина).

В 1975ом году Бейкер, Джил, Соловэй получили первый фундаментальный мета-результат о неразрешимости задачи P vs. NP с помощью регуляризируемых методов т.е. это первый результат, показывающий, что целый класс методов не может ответить на вопрос равенства P vs. NP (подробнее об этом написано здесь).

В 1979ом году Гэри и Джонсон напишут “Вычислительные машины и труднорешаемые задачи“, один из наиболее полных источников информации по NP-полноте и подробный каталог задач. Несмотря на то, что некоторые теоретические результаты в данный момент считаются устаревшими, это один из наиболее фундаментальных трудов в области вычислительной сложности.

Очень краткая история SAT-solvers

В 1960х Дэвис и Путман начали применять классически дедуктивные (говоря упрощенно, методы для доказательства теорем) методы для решения SAT (оригинальная работа).

В 1962ом году Дэвис, Патнем, Логеман, Лавленд предложили DPLL алгоритм, основанный на поиске с возвратом и распространении детерминированных вычислений (unit-propagation). Говоря упрощенно, алгоритм предполагал значение некоторой переменной равной истине и вычислял все детерминированные следствия подобного решения и повторял, пока не найдет решения. Данный алгоритм служил основой многих SAT solver’ов на протяжении десятилетий.

В 1992ом Селман, Левескью и Митчелл предложили метод локального поиска в статье GSAT. GSAT — означает Greedy SAT, локальный так как принимает решение о значении переменных на основе только локальной информации. Алгоритм начинал с произвольного назначения значений переменных и изменял значение переменной, если она давала наибольший прирост выполненных предложений. Впоследствии методы локального поиска в самых различных вариациях были интегрированы в большинство SAT solver’ов — в 1999 Хеглер Хус в своей PhD диссертации приводит обширное исследование по стохастическому локальному поиску и его применениям (работа доступна здесь).

В 1996ом Маркес-Силва (Marques-Silva) и Сакалах предложили алгоритм Conflict-Driven-Clause-Learning (CDCL), подобно DPLL он принимает решения о значении переменных и проводил детерминированные вычисления, с другой стороны он хранит в памяти граф имликаций и запоминает некоторые комбинации, которые не ведут к решению и может эффективно избегать «бесполезных» решений и эффективно отсекать пространство решений содержащее конфликт установленный ранее.

C 2001го начали появляться Locality Based Search SAT-solver’ы, эффективно выбирающие подпространства для полного поиска на основе локальной информации, такие как BerkMin (Berkley-Minsk) и многие другие.

Применение для доказательства гипотезы Коллатца

Действенная технология SAT-решателей может сработать с печально известной гипотезой Коллатца. Однако шансы на это не слишком велики. В последние несколько лет Марийн Хиюл использовал известную технологию компьютеризированных поисков доказательств под названием «SAT-решатель» (SAT от «satisfiability», то есть, «удовлетворяемость»), чтобы покорить впечатляющий список математических задач. Пифагоровы тройки в 2016 году, число Шура 5 в 2017, а недавно и гипотеза Келлера в седьмом измерении, о чём мы не так давно писали в статье “Компьютерный поиск помог разобраться с 90-летней математической задачей“. Однако теперь Хиюл, специалист по информатике из университета Карнеги-Меллона нацелился на ещё более амбициозную цель: гипотеза Коллатца, которую многие считают наиболее сложной из открытых задач в математике (и при этом, возможно, наиболее простой по формулировке). Другие математики, узнавая от меня о том, что Хиюл делает такую попытку, относились к этому с недоверием. «Не вижу, как можно решить эту задачу полностью при помощи SAT-решателя», — сказал Томас Хейлс из Питтсбургского университета, ведущий специалист в области компьютерных доказательств.

Эта технология, по сути, помогает математикам решать задачи – у некоторых из которых бывает бесконечное количество вариантов – превращая их в дискретные, конечные задачи. Однако Хейлс, как и другие, опасался недооценить Хиюла. «Он очень хорошо умеет находить хитроумные способы формулировать задачи на языке SAT. У него это прекрасно получается».

Скотт Ааронсон из Техасского университета в Остине, совместо с Хиюлом работающий над гипотезой Коллатца, добавил: «Марийн – это человек с молотом, то есть, с SAT-решателем, и, вероятно, наиболее достойный носитель этого молота во всём мире. И он пробует применять его практически ко всему». Но лишь время покажет, получится ли у него превратить гипотезу Коллатца в гвоздь.

Решение по методу SAT требует переформулировки задач на понятном компьютерам языке, использующем пропозициональную логику, а потом подключения компьютеров, которые решают, есть ли способ сделать эти высказывания истинными. Вот простой пример.

Допустим, вы – родитель, пытающийся организовать присмотр за ребёнком. Одна из ваших нянь может работать всю неделю, кроме вторника и четверга. Другая – кроме вторника и пятницы. Третья – кроме четверга и пятницы. Вам нужно, чтобы с ребёнком сидели во вторник, четверг и пятницу. Можно ли этого добиться?

Один из способов проверить это – превратить ограничения нянь в формулу, и скормить её в SAT-решатель. Программа поищет способ так распределить дни между нянями, чтобы формула оказалась истинной, или «удовлетворяемой» – то есть, так, чтобы вы получили три нужных вам дня. В случае успеха такой способ будет существовать.

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

«Сложно предсказать, когда задачу можно будет свести к огромному, но конечному вычислению», — сказал Ааронсон.

Гипотеза Коллатца – один из тех вопросов в математике, которые сначала вообще не кажутся похожими на задачу с нянями. Она предлагает следующее: взять любое число (целое, ненулевое). Если оно нечётное, умножить его на 3 и добавить 1. Если чётное, поделить на 2. В итоге вы получите новое число. Примените к нему те же правила, и продолжайте. Гипотеза предсказывает, что вне зависимости от стартового числа, вы в итоге получите 1, после чего застрянете в цикле: 1, 4, 2, 1.

И, несмотря на то, что с этой гипотезой работают почти 100 лет, математики не приблизились к её доказательству.

Но это не остановило Хиюла. В 2018 они с Аронсоном – в то время будучи коллегами по университету – получили грант от Национального научного фонда на применение SAT-решателя к гипотезе Коллатца.

Возьмите любое число. Если оно нечётное, умножить его на 3 и добавить 1. Если чётное, поделить на 2. В итоге вы получите новое число. Примените к нему те же правила, и продолжайте. Найдёте ли вы число, которое не приводит к 1? Можете попробовать самостоятельно.

Для начала Ааронсон, специалист по информатике, придумал альтернативную формулировку гипотезы Коллатца, т.н. «систему правил подстановки», с которой компьютерам было проще работать.

В системе правил подстановки вы работаете с набором символов, например, с буквами А, В и С. Вы используете их для формирования последовательностей: ACACBACB. Также у вас есть правила для преобразования этих последовательностей. Одно правило может говорить о том, что встречая АС, вы заменяете его на ВС. Другое может заменять ВС на ААА. Можно задать любое количество правил, определяющих любые преобразования.

Специалистам по информатике в основном нужно знать, всегда ли данная СП заканчивает работу. То есть, вне зависимости от того, с какой строки начинать, и в каком порядке применять правила, верно ли то, что строка в итоге превратится в состояние, в котором уже нельзя будет применить ни одного правила?

Ааронсон придумал СП с семью символами и 11 правилами, аналогичную гипотезе Коллатца. Если они смогут доказать, что его СП всегда заканчивает работу, они тем самым докажут, что гипотеза верна.

Чтобы превратить гипотезу Коллатца в задачу для SAT-решателя, Ааронсону и Хиюлу нужно было сделать ещё один шаг, связанный с матрицами, или массивами чисел. Им нужно было назначить уникальную матрицу каждому символу их СП. Такой подход – распространённый способ поисков доказательства того, что СП заканчивает работу – позволил бы им рассуждать о преобразованиях чисел через перемножение матриц. Семь матриц, обозначающих семь символов с СП должны были удовлетворять целому набору ограничений, отражающих соответствие 11 правил друг другу.

«Сначала вы пробуете подобрать матрицы, удовлетворяющие этим ограничениям, — сказал Эмре Йолчу, аспирант из университета Карнеги-Меллона, работающий над этой задачей с Хиюлом. – Если у вас получается, вы доказываете, что выполнение останавливается», и, следовательно, что гипотеза Коллатца верна.

На вопрос существования матриц, удовлетворяющих этим ограничениям как раз может ответить SAT-решатель. Ааронсон и Хиюл сначала запустили SAT-решатель на небольших матрицах 2х2. Рабочих вариантов они не нашли. Затем они попробовали матрицы 3х3. И снова безрезультатно. Они продолжали увеличивать размер матриц в надежде, что нужные найдутся.

Однако такой подход не может развиваться бесконечно, поскольку сложность поисков подходящих матриц растёт экспоненциально с ростом их размера. Хиюл предполагает, что современные компьютеры просто не справятся с матрицами размером более 12х12.

«Когда матрицы станут слишком сложными, вы не сможете решить задачу», — сказал он.

Хиюл всё ещё работает над оптимизацией поиска, пытаясь сделать его более эффективным, чтобы SAT-решатель мог проверять матрицы всё большего и большего размера. Они с коллегами работают над статьёй, подводящей итоги их текущим открытиям, но у них почти кончились идеи, и им, вероятно, вскоре придётся сдаться – по крайней мере, на какое-то время.

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

«Я просто оптимист, — сказал он. – Я часто чувствую, что мне повезёт, поэтому я просто пытаюсь и смотрю, насколько далеко мне удаётся продвинуться».

Автор: Вячеслав Голованов
Источник: https://habr.com/