Satisfiability Modulo Theories

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

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

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

Формально SMT формула — це формула в логіці першого порядку, в якій деякі функції і предикатні символи мають додаткову інтерпретацію, і задача полягає в тому, щоб визначити чи виконується дана формула. Іншими словами, на відміну від задачі розв'язності, замість булевих змінних SMT формула містить довільні змінні, а предикати — це булеві функції від цих змінних. Прикладами предикатів є лінійні порівняння (3x+ 2y - z \geq 4) або рівності, які включають терми, що не інтерпретуються, або функціональні символи (f(f(u, v), v) = f(u, v)), де f це деяка невизначена функція від двох аргументів. Предикати інтерпретуються згідно з теорією, якій вони належать. Наприклад, лінійні нерівності над дійсними змінними вираховуються згідно з правилами теорії лінійної дійсної арифметики, в той час як предикати над термами, які не інтерпретуються, і функціональними символами вираховуються по правилам теорії функцій з рівністю, які не інтерпретуються, (також відома як порожня теорія). SMT включає в себе також теорії масивів і списків (часто використовуються для моделювання і верифікації програм) і теорію бітових векторів (часто використовується для моделювання і верифікації апаратури). Можливі підкатегорії: наприклад difference logic — підкатегорія лінійної арифметики, в якій нерівності обмежені наступним чином (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 зі спеціалізованими для теорій розв'язувачами (Т-вирішувачі), які працюють з диз'юнкціями і кон'юнкціями предикатів з заданої теорії. Архітектура дубльованого DPLL(T) (англ. Dubbed 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.

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