Satisfiability Modulo Theories

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

У програмуванні, Satisfiability Modulo Theories (SMT) — це задача розв'язності для логічних формул з урахуванням теорій, які лежать в їх основі. Прикладами таких теорій для SMT формул є: теорії цілих та дійсних чисел, теорії списків, масивів, бітових векторів та ін.

Основні поняття[ред.ред. код]

Формально SMT формула — це формула в логіці першого порядку, в якій деякі функції і предикатні символи мають додаткову інтерпретацію, і задача полягає в тому, щоб визначити чи виконується дана формула. Іншими словами, на відміну від задачі розв'язності, замість булевих змінних SMT формула містить довільні змінні, а предикати — це булеві функції від цих змінних. Прикладами предикатів є лінійні порівняння () або рівності, які включають терми, що не інтерпретуються, або функціональні символи (), де це деяка невизначена функція від двох аргументів. Предикати інтерпретуються згідно з теорією, якій вони належать. Наприклад, лінійні нерівності над дійсними змінними вираховуються згідно з правилами теорії лінійної дійсної арифметики, в той час як предикати над термами, які не інтерпретуються, і функціональними символами вираховуються по правилам теорії функцій з рівністю, які не інтерпретуються, (також відома як порожня теорія). SMT включає в себе також теорії масивів і списків (часто використовуються для моделювання і верифікації програм) і теорію бітових векторів (часто використовується для моделювання і верифікації апаратури). Можливі підкатегорії: наприклад difference logic — підкатегорія лінійної арифметики, в якій нерівності обмежені наступним чином для змінних х і у і константи с.

Більшість SMT розв'язувачів (англ. SMT solvers) підтримують тільки формули без кванторів.

Виразна сила SMT[ред.ред. код]

SMT формула — це узагальнення булевої формули SAT, в якій змінні замінені предикатами з відповідних категорій. Тому SMT представляють більше можливостей для моделювання, ніж SAT формули. Наприклад, SMT формула дозволяє моделювати операції функції модулів мікропроцесора на рівні слів, а не на рівні бітів.

SMT розв'язувачі[ред.ред. код]

Перші спроби вирішення SMT задач були направленні на перетворення їх у SAT формули (наприклад 32-х бітні змінні кодувались 32-ма булевими змінними з кодуванням відповідних операцій над словами в низькорівневі операції над бітами) і вирішенням формули SAT розв'язувачем. Такий підхід має свої переваги — він дозволяє використовувати існуючі SAT розв'язувачі без змін (англ. As-Is), а також використовувати зроблені в них оптимізації. З іншої сторони втрата високорівневої семантики, яка лежить в основі теорій, означає, що SAT розв'язувач повинен докласти чималих зусиль, щоб вивести «очевидні» факти (такі як для додавання). Ця думка призвела до появи спеціалізованих SMT розв'язувачів, які інтегрують звичайні булеві докази в стилі алгоритму DPLL зі спеціалізованими для теорій розв'язувачами (Т-вирішувачі), які працюють з диз'юнкціями і кон'юнкціями предикатів з заданої теорії. Архітектура DPLL(T) передає функції булевого доказу DPLL SAT розв'язувачу, який в свою чергу взаємодіє з розв'язувачем теорії Т через визначений інтерфейс. Розв'язувач теорії Т повинен вміти перевіряти здійсненність кон'юнкцій із предикатів теорії, переданих з 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.

Посилання[ред.ред. код]