Русская Википедия:Задача выполнимости формул в теориях
Задача выполнимости формул в теориях (Шаблон:Lang-en, SMT) — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. Примерами таких теорий для SMT-формул являются: теории целых и вещественных чисел, теории списков, массивов, битовых векторов и т. п.
Основные понятия
Формально SMT-формула — это формула в логике первого порядка, в которой некоторые функции и предикатные символы имеют дополнительную интерпретацию. Задача состоит в том, чтобы определить выполнима ли данная формула. Другими словами, в отличие от задачи выполнимости булевых формул вместо булевых переменных SMT-формула содержит произвольные переменные, а предикаты — это булевы функции от этих переменных.
Примерами предикатов являются линейные неравенства (<math>3x+ 2y - z \geqslant 4</math>) или равенства, включающие так называемые неинтерпретируемые термы или функциональные символы: <math>f(f(u, v), v) = f(u, v)</math>, где <math>f</math> это некоторая неопределенная функция от двух аргументов. Предикаты интерпретируются согласно теории, которой они принадлежат. Например, линейные неравенства над вещественными переменными вычисляются по правилам теории линейной вещественной арифметики, тогда как предикаты над неинтерпретируемыми термами и функциональными символами вычисляются по правилам теории неинтерпретируемых функций с равенством (также называемой empty теорией). SMT включает также теории массивов и списков (часто используемые для моделирования и верификации программ) и теорию битовых векторов (часто используемые для моделирования и верификации аппаратуры). Возможны и подтеории: например, разностная логика — подтеория линейной арифметики, в которой неравенства ограничены следующим видом <math>x - y \leq c</math> для переменных <math>x</math> и <math>y</math> и константы <math>c</math>.
Большинство SMT-решателей (Шаблон:Lang-en) поддерживают только бескванторные формулы.
Выразительная сила SMT
SMT-формула — это обобщение булевой формулы SAT, в которой переменные заменены предикатами из соответствующих теорий. Поэтому SMT предоставляют больше возможностей для моделирования, чем формулы SAT. Например, SMT-формула позволяет моделировать операции функции модулей микропроцессора на уровне слов, а не на уровне битов.
SMT-решатели
Первые попытки решения SMT задач были направлены на преобразование их в SAT-формулы (например 32-битные переменные кодировались 32 булевыми переменными с кодированием соответствующих операций над словами в низкоуровневые операции над битами) и решением формулы SAT решателем. Такой подход имеет свои преимущества — он позволяет использовать существующие SAT решатели без изменений и использовать сделанные в них оптимизации. С другой стороны, потеря высокоуровневой семантики лежащих в основе теорий означает, что SAT решатель должен приложить немалые усилия, чтобы вывести «очевидные» факты (такие как <math>x + y = y + x</math> для сложения). Это соображение привело к появлению специализированных SMT-решателей, которые интегрируют обычные булевы доказательства в стиле алгоритма DPLL с решателями специализированными для теорий (T-решатели), работающие с дизъюнкциями и конъюнкциями предикатов из заданной теории.
Архитектура DPLL(T) передает функции булева доказательства SAT-решателю, который в свою очередь взаимодействует с решателем теории T. SAT-решатель генерирует модели, в которых часть входящих без отрицания литералов являются не булевыми переменными, а атомарными высказываниями некоторой, возможно многосортной, теории первого порядка. Решатель теории пытается найти противоречия в переданных ему моделях, и если такое противоречие не найдено, формула объявляется выполнимой. Для того чтобы такая интеграция работала, решатель теории должен участвовать в анализе конфликтов (Шаблон:Lang-en), предоставляя объяснения невыполнимости при возникновении конфликтов, которые запоминаются в решателе на основе DPLL-архитектуры. Так как количество SAT-моделей конечно, перебор приведёт к ответу за конечное время[1].
- Поддерживаемые и активно развивающиеся решатели: 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++.
Примечания
Литература
- Шаблон:Статья
- Шаблон:Книга
- D.Yurichev, Quick introduction into SAT/SMT solvers and symbolic execution
Ссылки
- SMT-LIB: библиотека
- SMT-COMP: Соревнование Satisfiability Modulo Theories
- Решающие процедуры — алгоритмический взгляд
- ↑ M. Armand, G. Faure, B. Gregoire, C. Keller, L. Thery, B. Werner. A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings. DOI 10.1007/978-3-642-25379-9_12
