Satisfiability Modulo Theories

В программировании, Satisfiability Modulo Theories (SMT) — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для SMT формул являются: теории целых и вещественных чисел, теории списков, массивов, битовых векторов и т.д.

Основные понятия

Формально SMT формула — это формула в логике первого порядка, в которой некоторые функции и предикатные символы имеют дополнительную интерпретацию и задача состоит в том, чтобы определить выполнима ли данная формула. Другими словами в отличие от задачи выполнимости вместо булевых переменных SMT формула содержит произвольные переменные, а предикаты это булевы функции от этих переменных. Примерами предикатов являются линейные сравнения ($3x+ 2y - z \geq 4$) или равенства, включающие так называемые неинтерпретируемые термы или функциональные символы ($f(f(u, v), v) = f(u, v)$), где $f$ это некоторая неопределенная функция от двух аргументов). Предикаты интерпретируются согласно теории, которой они принадлежат. Например, линейные неравенства над вещественными переменными вычисляются согласно правилам теории линейной вещественной арифметики, тогда как предикаты над неинтерпретируемыми термами и функциональными символами вычисляются по правилам теории неинтерпретируемых функций с равенством (также называемую empty теорией [1]). SMT включает также теории массивов и списков (часто используемые для моделирования и верификации программ) и теорию битовых векторов (часто используемые для моделирования и верификации аппаратуры). Возможны и подтеории: например difference logic — подтеория линейной арифметики, в которой неравенства ограничены следующим видом $x - y \leq c$ для переменных $x$ и $y$ и константы $c$.

Большинство SMT решателей (англ. SMT solvers) поддерживают только бескванторные формулы.

Выразительная сила SMT

SMT формула это обобщение булевой формулы SAT, в которой переменные заменены предикатами из соответствующих теорий. Поэтому SMT предоставляют больше возможностей для моделирования чем формулы SAT. Например, SMT формула позволяет моделировать операции функции модулей микропроцессора на уровне слов, а не на уровне битов.

SMT решатели

Первые попытки решения SMT задач были направлены на преобразование их в SAT формулы (например 32-х битные переменные кодировались 32-мя булевыми переменными с кодированием соответствующих операций над словами в низкоуровневые операции над битами) и решением формулы SAT решателем. Такой подход имеет свои преимущества — он позволяет использовать существующие SAT решатели без изменений (англ. as-is) и использовать сделанные в них оптимизации. С другой стороны потеря высокоуровневой семантики лежащих в основе теорий означает, что SAT решатель должен приложить немалые усилия, чтобы вывести "очевидные" факты (такие как $x + y = y + x$ для сложения). Это соображение привело к появлению специализированных SMT решателей, которые интегрируют обычные булевы доказательства в стиле алгоритма DPLL с решателями специализированными для теорий (T-решатели), работающие с дизъюнкциями и конъюнкциями предикатов из заданной теории.

Архитектура дублированного DPLL(T) (англ. Dubbed DPLL(T)) передает функции булева доказательства DPLL SAT решателю, который в свою очередь взаимодействует с решателем теории T через предопределенный интерфейс. Решатель теории T должен уметь проверять осуществимость конъюнкций из предикатов теории переданных из SAT решателя. Для того чтобы такая интеграция работала, решатель теории должен участвовать в анализе конфликтов (англ. conflict analysis), т.е. должен выводить новые факты из уже имеющихся, а также предоставлять объяснения невыполнимости при возникновении конфликтов. Другими словами, решатель теории должен быть инкрементальным (англ. incremental) и иметь возможность отката (англ. backtrackable).

• Поддерживаемые и активно развивающиеся решатели: Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, SatEEn, Spear, STP, UCLID, veriT, Yices, Z3.
• Другие: Argo-lib, Ario, CVC, CVC Lite, Fx7, haRVey, HTP, ICS, LPSAT, RDL, Sammy, Simplify, Simplics, STeP, SVC, Tsat++.

Литература

• Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006), "Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)", Journal of the ACM, 53(6), pp. 937–977.

Ссылки

• SMT-LIB: библиотека
• SMT-COMP: Соревнование Satisfiability Modulo Theories
• Решающие процедуры - алгоритмический взгляд