Hacker News Digest

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

На примере Судоку автор демонстрирует, как преобразовать правила игры в систему булевых ограничений. Для каждой клетки (i,j) и цифры k вводится переменная x_{i,j,k}, где true означает, что клетка содержит цифру k. Правила игры переводятся в ограничения: каждая клетка должна содержать ровно одну цифку (x_{i,j,1} ∨ x_{i,j,2} ∨ ... ∨ x_{i,j,9} и ¬x_{i,j,k} ∨ ¬x_{i,j,l} для k≠l), каждая цифра должна встречаться ровно один раз в строке, столбце и под-сетке. SAT-солвер находит удовлетворяющее всем этим ограничениям присвоение значений переменным, решая головоломку.

• SAT и MILP-солверы недооценены: первые хорошо знакомы инженерам, вторые — нет, хотя MILP позволяет естественно выразить оптимизацию и ограничения.
• Исторически открытые MILP-солверы отставали от коммерческих, что сдерживало их использование.
• SAT-солверы и MILP-солверы дополняют друг друга: SAT хорошо для задач «есть/нет», MILP — для задач оптимизации.
• Практически любую задачу можно выразить как MILP, и SAT-солверы могут быть использованы для решения MILP.

Булево значение почти всегда маскирует более точный тип.
Проверь, не дата-время ли это: is_confirmed лучше заменить на nullable confirmed_at. Вы получите момент подтверждения и сможете анализировать баги по времени.

Если поле описывает роль или статус (is_admin, failed), превращайте в enum.

enum UserRole { User, Admin, Guest, SuperAdmin }
enum JobStatus { Queued, Started, Failed, Done }

Enum упрощает добавление новых состояний и защищает от забытых веток.

Проверка прав тоже не должна возвращать bool.

enum PermissionCheck { Allowed, NotPermitted(reason: String) }

Так код читабельнее и можно вернуть причину отказа.

Когда же использовать bool? Только как временную переменную-флаг для сложного условия, чтобы не вычислять его дважды или дать имя.

• Основной спор: стоит ли хранить «события» как булевы флаги или как nullable-даты/enum’ы, чтобы не терять данные (время события).
• Противники: это нарушает KISS, раздувает схему и вводит двусмысленность (null = не случилось или ошибка?).
• Сторонники: булевы поля не «помнят» контекст, легко образуют недопустимые комбинации флагов, а дата или enum выразительнее.
• Для параметров функций булевы флаги считаются плохо читаемыми; спасают именованные аргументы, отдельные функции или бит-маски.
• Встраиваемые/индустриальные системы часто считают булевы типы оптимальными по памяти и не применяют совет к себе.