Задача выполнимости формул в теориях

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

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

Формально SMT-формула — это формула в логике первого порядка, в которой некоторые функции и предикатные символы имеют дополнительную интерпретацию. Задача состоит в том, чтобы определить выполнима ли данная формула. Другими словами, в отличие от задачи выполнимости булевых формул вместо булевых переменных SMT-формула содержит произвольные переменные, а предикаты — это булевы функции от этих переменных.

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

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

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

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

SMT-решатели

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

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

• Поддерживаемые и активно развивающиеся решатели: 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. Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T) // Journal of the ACM. — 2006. — Т. 53, № 6. — P. 937—977.
• Biere, A. and Gomes, C.P. Theory and Applications of Satisfiability Testing - SAT 2006: 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings. — Springer, 2006. — P. 142-155. — 438 p. — ISBN 9783540372066.
• D.Yurichev, Quick introduction into SAT/SMT solvers and symbolic execution

Ссылки

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