Математическая логика
Пропозициональная логика
2003 год. Intel Pentium 4. Ошибка в логике блока умножения чисел с плавающей точкой. Цена отзыва - 475 миллионов долларов. После этого Intel начала верифицировать каждый транзистор через SAT-солверы. Те же самые формулы, которые доказывают `False -> True = True` - проверяют что CPU считает 2+2=4 на любом из 10^18 возможных наборов входных данных. Пропозициональная логика - не абстракция для учебников, а единственный способ доказать корректность чипа до его выхода.
- **SAT-солверы (Z3 от Microsoft, CaDiCaL)**: верификация процессоров Intel/AMD - формулы с ~10^6 переменных, решаются за секунды несмотря на NP-полноту
- **Amazon AWS**: TLA+ и SMT-солверы проверяют политики IAM и протоколы распределённых систем - формальная верификация в продакшне на миллиарды запросов
- **LLM chain-of-thought**: GPT-4 при рассуждении имитирует логический вывод (modus ponens, транзитивность) - Kahneman System 2 через вероятностную машину
- **Chip design**: AMD и Apple Silicon используют SAT для проверки корректности схем - до миллиарда транзисторов, ни один нельзя не проверить
Логические связки
Каждый `if (x > 0 && y != null)` - это пропозициональная логика. Каждый LLVM-оптимизатор, упрощающий `!(a && b)` в `(!a || !b)` - это де Морган. Каждый SMT-солвер, доказывающий что AWS IAM-политика не допускает несанкционированный доступ - это SAT. **Пропозициональная логика** - язык для работы с высказываниями True/False и **связками** (connectives), которые их комбинируют. Язык, лежащий под половиной современного программирования.
| Связка | Символ | Чтение | Python | Пример |
|---|---|---|---|---|
| Отрицание | NOT p | не p | not p | не идёт дождь |
| Конъюнкция | p AND q | p и q | p and q | дождь и ветер |
| Дизъюнкция | p OR q | p или q | p or q | дождь или снег |
| Импликация | p -> q | если p, то q | not p or q | если дождь, то зонт |
| Эквиваленция | p <-> q | p тогда и только тогда, когда q | p == q | чётное <-> делится на 2 |
**Приоритет связок** (от высшего к низшему): NOT > AND > OR > -> > <->. Без скобок выражение `NOT p AND q OR r` читается как `((NOT p) AND q) OR r`. Скобки всегда помогают прояснить смысл.
**Импликация** - самая контринтуитивная связка. `p -> q` ложна ТОЛЬКО когда p истинна, а q ложна. В частности, `False -> anything = True` (ex falso quodlibet - из лжи следует всё). Это не баг - это определение, необходимое для математической непротиворечивости.
Пропозициональные переменные (p, q, r) - это **атомы**. Из атомов и связок строятся **формулы**: `(p -> q) AND (q -> r) -> (p -> r)` - закон транзитивности импликации. Формула бывает **тавтологией** (всегда True), **противоречием** (всегда False) или **выполнимой** (True при некоторых значениях). SAT-солвер занимается именно третьим случаем - и именно он стоит миллиарды в chip verification.
Чему равно значение `False -> True`?
Таблицы истинности
**Таблица истинности** - брутфорс проверки формулы: перебираем ВСЕ комбинации значений, вычисляем результат. Для n переменных - 2^n строк. Результат всегда True - тавтология. Метод безупречный и нескалируемый одновременно.
**Экспоненциальный взрыв**: для 10 переменных - 1024 строки, для 20 - миллион, для 100 - больше атомов во Вселенной. Таблица истинности работает, но не масштабируется. Для больших формул нужны алгоритмические методы (DPLL, CDCL).
**Законы де Моргана** - фундамент: NOT(p AND q) = (NOT p) OR (NOT q) и NOT(p OR q) = (NOT p) AND (NOT q). LLVM и GCC используют их тысячи раз в секунду при оптимизации условных выражений в машинный код. Программист знает де Моргана интуитивно - теперь есть формальное имя.
| Закон | Формула | Программистский пример |
|---|---|---|
| De Morgan 1 | NOT(p AND q) = NOT p OR NOT q | !(a && b) == (!a || !b) |
| De Morgan 2 | NOT(p OR q) = NOT p AND NOT q | !(a || b) == (!a && !b) |
| Двойное отрицание | NOT NOT p = p | !!x == x |
| Дистрибутивность | p AND (q OR r) = (p AND q) OR (p AND r) | Аналог a*(b+c)=ab+ac |
| Контрапозиция | (p -> q) = (NOT q -> NOT p) | if rain→wet, then dry→no rain |
Сколько строк в таблице истинности для формулы с 4 переменными?
Нормальные формы
Одну и ту же логическую формулу можно записать по-разному. **Нормальные формы** - канонические представления для алгоритмической обработки. CNF - стандарт SAT-солверов по всему миру. DNF - язык баз знаний и классификаторов. Две формы, два мира применений.
**CNF** - язык SAT-солверов. Z3 от Microsoft, MiniSat, CaDiCaL - все принимают CNF на входе. Любую формулу можно привести к CNF за полиномиальное время через Tseytin transformation. Именно этот формат позволяет верифицировать корректность ARM-чипов Apple M-серии.
| Свойство | CNF | DNF |
|---|---|---|
| Структура | AND of (OR of literals) | OR of (AND of literals) |
| Проверка SAT | NP-полная | Полиномиальная (хотя бы 1 конъюнкт True) |
| Проверка TAUT | Полиномиальная (все клаузы True) | NP-полная |
| Размер | Может быть экспоненциальной | Может быть экспоненциальной |
| Применение | SAT-солверы, верификация | Базы знаний, классификация |
**Tseytin transformation** - способ преобразования в CNF с полиномиальным ростом размера. Идея: вводим новые переменные для подформул. Формула `(a ∧ b) ∨ (c ∧ d)` получает переменные x = (a ∧ b), y = (c ∧ d), и CNF для x ∨ y плюс определения x, y.
Какая из формул находится в CNF?
Satisfiability (SAT)
Дана формула в CNF. Существует ли набор значений переменных, при котором она истинна? Это **SAT problem** - первая задача, доказанная **NP-полной** (Кук, 1971). Теоретически неподъёмная. Практически - современные солверы решают формулы с миллионом переменных за секунды. Расхождение между worst-case теорией и реальными инстанциями - одна из главных загадок CS.
**DPLL** (Davis-Putnam-Logemann-Loveland, 1962) - классический алгоритм для SAT. Идея: выбираем переменную, присваиваем True или False, упрощаем формулу, рекурсивно решаем. Оптимизации: **unit propagation** (если клауза из одного литерала - его значение определено) и **pure literal elimination**.
Несмотря на NP-полноту, современные SAT-солверы (Z3, CaDiCaL, Kissat) решают промышленные задачи с **миллионами** переменных. Intel и AMD - верификация процессоров. Amazon AWS и Microsoft Azure - formal verification облачных систем через TLA+. Apple - верификация M-серии чипов. SMT-солверы (SAT + теории) идут дальше: symbolic execution, automated theorem proving, анализ безопасности кода.
| Применение SAT | Пример | Переменных |
|---|---|---|
| Верификация чипов | Intel CPU correctness | ~10⁶ |
| Планирование | Расписание экзаменов | ~10⁴ |
| Криптоанализ | Поиск коллизий MD5 | ~10⁵ |
| Конфигурация | Linux kernel config | ~10⁴ |
| Formal verification | Proofs of programs | ~10⁵ |
SAT - это не абстракция. Любая задача из NP сводится к SAT: раскраска графа, задача о рюкзаке, Судоку, маршрутизация. Если задача звучит как «найти значения, удовлетворяющие набору ограничений» - она кодируется в SAT. Именно так Qualcomm верифицирует Snapdragon: ограничения чипа → CNF → SAT-солвер → «все пути корректны» или «найден контрпример».
Импликация p → q означает причинно-следственную связь: p вызывает q
Импликация p → q - это логическая связка, эквивалентная ¬p ∨ q. Она ложна только когда предпосылка истинна, а следствие ложно
В разговорном языке «если дождь - улица мокрая» подразумевает причинность. В логике p → q - ограничение: нельзя одновременно p = True и q = False. «Если 2+2=5, то луна из сыра» - логически истинное высказывание (False → anything = True). Именно это свойство используется в SAT: формула UNSAT - значит из неё следует что угодно, включая False. Так солвер находит противоречие в схеме чипа.
Формула (p) ∧ (¬p). Является ли она выполнимой?
Ключевые идеи
- **Связки** (NOT, AND, OR, ->, <->) - алфавит формальных рассуждений: тот же язык в `if/else`, SQL WHERE и firewall-правилах
- **Таблицы истинности** дают исчерпывающую проверку за O(2^n) - работают для 10 переменных, не работают для 10^6
- **CNF** (AND of ORs) - язык SAT-солверов; через неё кодируется всё: от Судоку до корректности процессора
- **SAT** - первая NP-полная задача (Кук, 1971), но Z3, MiniSat и CaDiCaL решают промышленные задачи с миллионами переменных за секунды - теория и практика здесь расходятся
Связанные темы
Пропозициональная логика - фундамент для более мощных логических систем:
- Предикатная логика первого порядка — Расширяет пропозициональную логику кванторами (для всех, существует) и предикатами
- Естественный вывод — Формальная система доказательств для пропозициональных и предикатных формул
Вопросы для размышления
- Почему `False -> True = True`? Как это свойство используется в SAT-солверах при поиске противоречий?
- Задача Судоку кодируется в SAT: каждая клетка - переменная, каждое ограничение - клауза. Сколько клауз потребуется для стандартной 9x9 сетки?
- Почему проверка SAT (выполнимости) NP-полная, а проверка тавтологии - co-NP? В чём практическая разница для верификации программ?