Поиск множеств «входных» переменных в булевой формуле. Множество «входных» переменных — такое множество переменных, что при подстановке значений всем переменным множества значения для всех остальных переменных формулы определяются однозначно. Иногда такие переменные называют ещё «существенными».
Множество входных переменных, если оно известно, может быть использовано для прогнозирования времени работы и распараллеливания решения задачи SAT для конкретной формулы. Этим занимаются специальные методы декомпозиции по входам.
Задача SAT — Дана булева формула в КНФ. Найти набор значений переменных, при котором формула истинна, или доказать, что такого назначения не существует.
Задача NP-полна, если она принадлежит классу NP и любая задача из NP сводится к ней за полиномиальное время. Задача SAT NP-полна.
SAT-решатель — программа, решающая задачу SAT.
Процедура распространения единичных литералов (Unit Propagation — UP) — алгоритм, позволяющий упростить формулу, заданную в КНФ.
Основной алгоритм решения SAT — Conflict-Driven Clause Learning (CDCL), базирующийся на алгоритме DPLL (по именам учёных), в основе которого лежит процедура распространения единичных литералов (UP).
Задача SAT применяется во многих областях, в частности, при решении оптимизационных задач или верификации программ и схем. Верификация сводится к построению булевой модели системы, после чего с помощью решения задачи SAT можно проверить существование или отсутствие удовлетворяющего означивания переменных, что эквивалентно поиску ошибок в программе или схеме.
Так как задача SAT является NP-полной, SAT-решатель может работать экспоненциально долго (т. н. heavy-tailed behaviour). С этим можно бороться, применяя параллельность с помощью специальных методов декомпозиции. Специальные методы построения декомпозиций позволяют декомпозировать задачу на множество независимых подзадач, решаемых параллельно, а также построить точные оценки времени решения такой декомпозиции. Однако такие методы требуют знания множества «входов».
- python
$\ge$ 3.9
git pull --recurse-submodules
cd abc
make
cd ..
cd aiger
./configure.sh && make
cd ..
pip install -r requirements.txt
Любой код необходимо запускать из корня проекта.
Для начала необходимо найти где-то примеры логических схем. Используются ресурсы с соревнований по формальной верификации схем, они добавлены в репозиторий сабмодулями — benchmarks, iwls2024-ls-contest, hdl-benchmarks. Также для тестирования на произвольных формулах использовался набор данных с SAT competition 2021. Формулы слишком большие, загружать скриптом
Затем необходимо найденные схемы переконвертировать из форматов для схем в формат для булевых формул в КНФ. Этим занимается
модуль тестов. Поддерживаются два формата для схем — .aig (And-Inverter Graph) и .v (Verilog).
Используется специальная утилита. Она доступна в Test PyPI.
Таким образом, схема из бинарного формата .aig или формата для схем .v конвертируется в ASCII-формат .aag
с помощью утилиты aiger,
затем из .aag конвертируется в .cnf в общепринятом формате DIMACS с помощью утилиты aigerox.
Чтобы исключить ошибки при конвертации, после этого шага формула проверяется SAT-солвером на выполнимость с ограничением по времени в
После этого тесты готовы, можно запускать решения и проверки. Для запуска решений используются скрипты.
Все решения можно запустить из CLI, передав в качестве первого аргумента имя .cnf файла, где лежит интересующая формула.
У evolution и orchestra есть хелперы для аргументов командной строки, можно посмотреть, что они принимают.
В fast_orchestra есть единственный второй аргумент: --fasten, который ухудшает ответ, но ускоряет решение.
Пример запуска evolution:
python3 evolution.py tests/cnf/adder.cnf -s 256 -g 1000 -m conflictsПример запуска extractor:
python3 extractor.py tests/cnf/adder.cnf --non-schemasЗатем ответы, найденные решениями, можно оценить и автоматически составить отчёт, этим занимается модуль отчётов. Отчет сохраняется в reports, чтобы не засорять репозиторий, папка игнорируется гитом.
Для сбора статистики по конфликтам в подстановках для различных схем используется скрипт. В папку stats записываются наблюдения о конфликтах на различных размерах множеств для разных схем. На этих наблюдениях затем можно построить графики с помощью графического модуля.
-
fullscan_border: полный перебор всех возможных подмножеств
в порядке увеличения размера подмножества. На шаге
$k$ перебираются все подмножества мощности$k$ , если найден вход, перебор прекращается. Худший случай, очевидно$\theta(4^n)$ . ($n$ – количество переменных в формуле), так как$2^n$ возможных подмножеств и в каждом подмножестве необходимо перебрать все возможные значения переменных. По факту же если вход совсем небольшой, отработает быстро. -
fullscan_3n: полный перебор за
$O(3^n)$ . Минус по сравнению с fullscan_border в том, что нет отсечения при найденном маленьком размере входа, и время всегда экспоненциальное. - Остальные переборные решения, как правило, тоже содержат префикс
fullscan, и являются различными оптимизациями с отсечениями. Не стоит обращать на них особенного внимания, так как на реальных размерах схем они всё равно совершенно неэффективны.
- evolution: эволюционный алгоритм 1+1, особь — множество переменных, мутация — равновероятная замена каждого элемента множества на ещё не используемый, функция приспособленности — конфликты и количество выведенных на некоторых подстановках.
- cut_conflicts: использует функционал SAT-решателя по нахождению конфликтующих переменных. Строим большое множество переменных, делаем на нём несколько подстановок, исключаем самую часто конфликтующую переменную, повторяем до тех пор, пока не достигнем нужного размера множества.
- greedy_expansion: алгоритм жадного расширения, берём какое-то стартовое множество, пытаемся расширить его в сторону тех переменных, которые дают меньше всего конфликтов.
- orchestra: комбинация greedy_expansion и evolution, сначала расширяемся в сторону минимальных конфликтов, затем мутируем получившиеся множества.
- fast_orchestra: ускоренная комбинация greedy_expansion, evolution и cut_conflicts, сначала расширяемся в сторону минимальных конфликтов, затем мутируем получившееся множество, затем исключаем конфликтующие переменные.
- extractor: модуль для внешнего использования, меняет конфигурации поиска входов в зависимости от размера и структуры схем — для большой схемы запускает упрощённый поиск, который работает быстрее, но находит ответ хуже и наоборот.
- Таких нет, это
$NP-NP$ задача.