[VLSI CAD] MiniSAT?

Задача удовлетворимости (SAT) вкратце сводится к следующему вопросу:

Можно ли установить переменные в True / False так, чтобы заданная булева формула была истинной?

Например, если дана формула f(x,y,z)=(x || y) & (!x || z),

• Поиск того, как задать True/False для x, y и z так, чтобы вся формула была True, является задачей SAT.

Это кажется достаточно простым, но когда число переменных исчисляется тысячами или десятками тысяч,

• а ограничений - сотнями тысяч,
• это становится полным исследованием невозможным.

Страница MiniSat

by Niklas Eén, Niklas Sörensson

2. Что за SAT-решатель MiniSat

MiniSat - это высокопроизводительный SAT-решатель на основе CDCL.

Особенности:

• CDCL (Conflict-Driven Clause Learning)
• Очень маленькая кодовая база
• Быстрый и стабильный
• Легко встраивается как библиотека в другие инструменты

Так, хотя MiniSat может использоваться самостоятельно, на самом деле он чаще всего применяется для следующих целей.

• Внутренний движок инструмента формальной верификации
• Двигатель принятия решений для инструмента EDA
• Исследовательский прототип базового решателя
• Бэкэнд SAT-движка решателяSMT/PB

Т.е,

MiniSat - это скорее "стандартный движок в мире SAT-решателей"

3. Но реальный мир не исчерпывается SAT

Проблема в том, что реальные ограничения не всегда являются булевыми.

Например, это ограничение не является SAT:

3a + 2b + c ≥ 4

Здесь a, b и c - булевы переменные, но само выражение является ограничением с целочисленными весами.

Такое ограничение называется псевдобулевым (PB) ограничением.

Проблемы PB характеризуются следующим:

• Переменные являются булевыми
• Ограничения являются линейными целочисленными неравенствами
• Зачастую имеют оптимизационную задачу (min/max)

4. Основная идея MiniSat+

MiniSat+ не является новым решателем.<У него есть только одна основная идея:

Перевести ограничение PB в SAT, а затем решить его с помощью MiniSat

Такова структура:

PB-задача
↓ (перевод)
SAT-задача
↓
MiniSat

MiniSat+ отвечает за этот переводной слой.

5. Как преобразовать PB → SAT

MiniSat+ использует следующие логические схемы для преобразования PB-ограничений в SAT.

• BDD (двоичная диаграмма принятия решений)
• Согласованная сеть
• Сортировочная сеть

Ключевые моменты:

• Создайте логическую схему
• Определите, удовлетворяется ли ограничение PB
• Преобразуйте схему в CNF с помощью преобразования Цейтина
• Введите результат в MiniSat

Так,

"Создать схему, проверяющую ограничения,

6. Зачем переходить на SAT

Вы можете спросить, почему бы просто не написать свой собственный решатель PB?

• Решатели SAT оптимизировались десятилетиями
• Обучение клаузеров, эвристика, распространение очень мощны
• Для "почти SAT-задач"
  • Преобразование SAT + MiniSat часто быстрее, чем собственные решатели PB
    • В основном булевы структуры
    • Некоторые ограничения по весу/счету
  • Формальная проверка эквивалентности
  • Выбор минимального набора исправлений в ECO
  • Синтез на основе ограничений
  • Проблемы выбора ресурсов/опций
  • Некоторая внутренняя логика принятия решений STA/CDC/DFT
  • MiniSat
    → Высокопроизводительный булевский решатель SAT
    → Быстрый движок для решения задач выбора
  • MiniSat+
    → Целочисленные взвешенные ограничения (PB) к SAT. Использует возможности MiniSat
  • Зачем его использовать
    → SAT-решатель по-прежнему является самым мощным механизмом комбинаторного поиска
    → Структурно хорошо подходит для EDA/верификации

особенно для задач EDA/верификации:Подход MiniSat+ хорошо работает на этих структурах.

7. Где он используется с точки зрения EDA

С точки зрения инженера, семейство MiniSat идеально подходит для решения следующих задач.Общим для всех них является то, что их объединяет.

Переменные выбора + ограничения + комбинаторный взрыв

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

8. Резюме в одном абзаце