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) передає функції булевого доказу 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.

Посилання

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