algorithms · advanced · 8d
Прувер по таблицам истинности
Преврати логику, которую ты изучал на бумаге, в работающий движок: распарси формулу пропозициональной логики в дерево, обойди все наборы значений и построй её таблицу истинности, а затем реши, тавтология ли она, выполнима ли и эквивалентна ли другой формуле. Логика — это место, где строгость становится механической, и написать машину, которая проверяет рассуждение, — самый верный способ понять, почему рассуждение верно. В итоге у тебя будет маленький, но честный проверяльщик теорем, которому ты доверяешь, потому что собрал каждый его шаг сам.
Результат
Инструмент командной строки, который читает формулу пропозициональной логики в небольшом синтаксисе (переменные, ¬, ∧, ∨, →, ↔), печатает её полную таблицу истинности, сообщает «тавтология / выполнима / противоречие», проверяет эквивалентность двух формул и — как стретч — отвечает на вопрос о выполнимости через поиск в стиле DPLL и проверяет короткое доказательство методом естественного вывода.
Этапы
0/5 · 0%- 01От текста к дереву
Формула вроде (p → q) ∧ ¬r — это всего лишь строка, пока ты не придашь ей структуру. Разбей её на токены, а затем распарси в абстрактное синтаксическое дерево, где каждый узел — это связка, а его потомки — подформулы, которые она соединяет. Сложность в приоритете и ассоциативности: ¬ связывает сильнее всего, затем ∧, затем ∨, затем →, затем ↔, а → ассоциируется вправо. Ошибись здесь — и p → q → r тихо будет значить не то, что нужно, поэтому запиши грамматику до того, как писать парсер, и отклоняй некорректный ввод громко, а не угадывай. Это дерево — стержень всего дальнейшего; каждый следующий этап просто обходит его.
Критерии готовности- Парсинг (p → q) ∧ ¬r даёт дерево, корень которого — ∧, в соответствии с задокументированным приоритетом и правоассоциативным →.
- Некорректный ввод (несбалансированные скобки, висящий оператор) вызывает понятную ошибку парсинга, а не возвращает неправильное дерево.
- 02Вычисли при наборе значений, затем построй таблицу
Теперь придай дереву смысл. Напиши вычислитель, который при заданном наборе значений переменных обходит дерево снизу вверх и возвращает true или false для всей формулы. Затем перебери все 2^n наборов для n различных переменных и собери по строке на каждый набор — это и есть таблица истинности. Две предостережения, с которыми стоит столкнуться сейчас: таблица растёт экспоненциально, поэтому n намеренно мало; и переменные нужно собирать из дерева в устойчивом порядке, чтобы столбцы совпадали. Когда ты напечатаешь полную таблицу для ¬(p ∧ q) и сверишь её со своей головой, движок перестанет быть догадкой.
Критерии готовности- При формуле и явном наборе значений вычислитель возвращает правильное булево значение, рекурсивно обходя дерево.
- Печать таблицы для формулы с 2 или 3 переменными показывает все 2^n строк со столбцами переменных в устойчивом порядке и со столбцом результата.
- 03Реши: тавтология, выполнимость, эквивалентность
Три важнейших вопроса логики выпадают прямо из таблицы. Формула — тавтология, если истинна каждая строка; противоречие, если ложна каждая строка; и выполнима, если истинна хотя бы одна строка. Две формулы эквивалентны ровно тогда, когда A ↔ B — тавтология; это самое чистое определение, которое тебе встретится. Реализуй все четыре проверки поверх своего перебора и возвращай свидетельствующий набор значений, когда что-то выполнимо, потому что «да, и вот почему» лучше голого «да». Это момент, когда инструмент оправдывает своё имя: теперь он решает рассуждения, а не просто описывает их.
Критерии готовности- Проверки «тавтология», «противоречие» и «выполнима» согласуются с таблицей на известных случаях (p ∨ ¬p, p ∧ ¬p, p ∧ q).
- equivalent(A, B) возвращает true ровно тогда, когда A ↔ B — тавтология, а проверка выполнимости возвращает свидетельствующий набор значений.
- 04Ищи умнее: крошечный DPLL
Таблица истинности проверяет все 2^n строк, даже когда ответ очевиден уже после первых нескольких. Настоящие SAT-решатели так не делают — они ищут. Преобразуй формулу в КНФ (конъюнкцию дизъюнктов), а затем напиши поиск с возвратом в стиле DPLL: выбери неназначенную переменную, попробуй true, протолкни очевидные следствия (юнит-пропагация: клауза из одного литерала вынуждает этот литерал) и откатывайся, когда клауза становится пустой. Это тот же перебор, но с отсечениями, и на формулах, где таблица захлебнётся, DPLL всё ещё отвечает. Увидеть, как твой рекурсивный поиск выдаёт тот же вердикт о выполнимости, что и таблица, но быстрее, — вот награда: умный поиск побеждает лишние строки.
Критерии готовности- Формулы преобразуются в КНФ, и поиск DPLL выдаёт тот же вердикт SAT/UNSAT, что и метод таблицы истинности, на общих тестовых случаях.
- Юнит-пропагация и возврат реализованы так, что на специально выбранной формуле поиск посещает заметно меньше состояний, чем полная таблица из 2^n строк.
- 05Проверь доказательство, а не только истинностное значение
Таблицы истинности говорят тебе, что заключение следует; доказательство говорит, почему, шаг за шагом. Построй проверяльщик для нескольких правил естественного вывода — modus ponens (из A и A → B выводим B), введение конъюнкции, удаление конъюнкции, может быть, снятие допущения для введения →. Проверяльщик читает список строк, каждая из которых ссылается на правило и номера предыдущих строк, от которых зависит, и убеждается, что каждый шаг — законное применение. Глубокая идея, которую ты здесь почувствуешь, — разрыв между семантической истинностью (таблица) и синтаксической доказуемостью (доказательство): корректный набор правил никогда не выводит не-тавтологию, а поймать незаконный шаг — и есть вся работа проверяльщика доказательств.
Критерии готовности- Корректное доказательство с использованием поддерживаемых правил принимается, а доказательство с одним незаконным шагом отклоняется с указанием плохой строки.
- Заключение любого принятого доказательства проверяется на то, что оно действительно является тавтологией его посылок, перекрёстно сверяясь с движком таблиц истинности.
Стартер
- README.md
- src/prover.ts
- test/prover.test.ts
Распакуй, реализуй заглушки, затем гоняй тесты, пока не позеленеют: bun test
Рубрика
| Джуниор | Миддл | Сеньор | |
|---|---|---|---|
| Корректность парсера | Обрабатывает переменные и подмножество операторов, но тихо выдаёт неправильное дерево для граничных случаев — например, путает приоритет & и | или парсит -> лево-ассоциативно. | Реализует все пять операторов с правильной цепочкой приоритетов (! > & > | > -> > <->), право-ассоциативный ->, и скобки. Бросает исключение на некорректном вводе — висячий оператор, незакрытая скобка. | Парсер — чистая реализация рекурсивного спуска или алгоритма сортировочной станции с явной грамматикой, записанной до кода; приоритет и ассоциативность структурно обеспечиваются грамматикой, а не заплатками из особых случаев. Сообщения об ошибках называют неожиданный токен и его позицию. Свойственные тесты подтверждают обходимость (parse → print → parse) на большом наборе случайных формул. |
| Вычисление и перебор 2^n наборов | Вычисляет три базовые связки (not, and, or), обходя дерево. Может напечатать таблицу истинности для двухпеременной формулы, но извлечение переменных произвольно и может дублировать столбцы. | Корректно вычисляет все пять связок, включая вакуумную истинность false -> * и двустороннее равенство <->. Извлекает переменные из AST в устойчивом отсортированном порядке и генерирует все 2^n наборов без сторонних библиотек. | Может сформулировать точную сложность (O(2^n · |формула|) по времени, O(|формула| + n) по памяти без учёта таблицы), объяснить, где это перестаёт масштабироваться (n ≈ 20–25 на практике), и указать направление BDD или SAT для большего n. Генератор наборов — цикл на битовых масках, а не рекурсия, чтобы избежать давления на стек при большом n. |
| Классификация и эквивалентность | classify возвращает результат, подсчитывая истинные строки, но может путать «выполнима» и «контингентна», или пропускать, что формула без переменных вакуумно является тавтологией. | classify корректно различает тавтологию (все строки истинны), противоречие (все строки ложны) и контингентность (оба вида строк есть), включая граничные случаи с одной переменной. equivalent прерывает обход на первом несовпадающем наборе, а не собирает все строки сначала. | Может доказать, что equivalent(a, b) — это ровно classify(a <-> b) == tautology: оба пути кода тестируются и дают одинаковый ответ на одних парах формул. Может объяснить, почему эквивалентность — не то же самое, что синтаксическое тождество (a->b и !a|b — разные деревья, но одинаковая семантика), и связать это с ролью нормальных форм: две формулы в одной КНФ или ДНФ синтаксически тождественны тогда и только тогда, когда семантически эквивалентны. |
Эталонный разбор (спойлер)
Рекурсивный спуск против алгоритма сортировочной станции: рекурсивно-нисходящий парсер отображает каждый уровень приоритета в одну функцию (parseIff → parseImpl → parseOr → parseAnd → parseNot → parseAtom); стек вызовов структурно обеспечивает приоритет. Алгоритм сортировочной станции достигает того же с явным стеком операторов и является итеративным, избегая глубокой рекурсии на длинных цепочках. Для грамматики с пятью уровнями оба варианта подходят; сортировочная станция чаще встречается в интерпретаторах языков выражений, рекурсивный спуск — в компиляторах и линтерах, где грамматика читается прямо из кода.
Почему 2^n строк и где это перестаёт масштабироваться: перечисление всех наборов значений экспоненциально по числу различных переменных. До n ≈ 20 это быстро (1M строк); при n = 30 занимает секунду; при n = 50 нереально. Реальные SAT-решатели (DPLL, CDCL) и верификаторы моделей выходят из полного перечисления, рассуждая символически: они выбирают переменную, распространяют следствия (юнит-пропагация) и откатываются только при обнаружении противоречия — посещая крошечную долю 2^n состояний на большинстве практических случаев. Бинарные диаграммы решений (BDD) идут другим путём: они представляют булеву функцию как ориентированный ациклический граф, сжатый совместным использованием подрезультатов, что даёт полиномиальную по времени проверку эквивалентности для многих семейств формул.
Нормальные формы КНФ и ДНФ: конъюнктивная нормальная форма (КНФ) — это И дизъюнктов; дизъюнктивная нормальная форма (ДНФ) — это ИЛИ конъюнктов. Каждая пропозициональная формула имеет обе. КНФ — это входной язык SAT-решателей (формат DIMACS); ДНФ позволяет напрямую читать выполняющие наборы (каждый конъюнкт — один свидетель). Наивное преобразование в КНФ через распределение И над ИЛИ может дать экспоненциальный взрыв — кодирование Цейтина избегает этого, вводя свежие переменные для каждой подформулы, сохраняя КНФ линейной по размеру исходной формулы ценой добавления вспомогательных переменных, отсутствующих в оригинале.
Семантическая и синтаксическая эквивалентность: две формулы семантически эквивалентны, когда совпадают на каждом наборе значений — здесь проверяется через equivalent(a, b). Они синтаксически тождественны только когда их деревья разбора совпадают узел-за-узлом. Нормальные формы заполняют разрыв: если привести обе формулы к канонической КНФ или ДНФ (например, сортируя литералы и дизъюнкты), синтаксическое тождество становится достаточным (и эффективным) тестом семантической эквивалентности. Именно так насыщение равенствами и движки перезаписи e-графов решают эквивалентность без перебора таблиц истинности.
Сделай по-сеньорски
- Добавь кодирование Цейтина, чтобы преобразование произвольной формулы в КНФ оставалось линейным по размеру, а не взрывалось, и подавай результат в свой DPLL-решатель.
- Сгенерируй минимальную ДНФ или упрощённый эквивалент из выполняющих строк, чтобы инструмент мог не только решать, но и переформулировать формулу в более чистом виде.
- Проверь DPLL-решатель свойствами против перебора по таблице на тысячах случайных формул, утверждая, что они всегда сходятся по SAT/UNSAT.