WikiSort.ru - Компьютерные программы

ПОИСК ПО САЙТУ | о проекте

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

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

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

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

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

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

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

SMT-решатели

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

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

Примечания

  1. 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

Литература

  • 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.

Ссылки

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .




Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2020
WikiSort.ru - проект по пересортировке и дополнению контента Википедии