SMTproblemen

SMT-problemen (Satisfiability Modulo Theories) zijn beslissingsproblemen die bestaan uit een logische formule met booleaanse variabelen die verbonden zijn met achtergrondtheorieën. De achtergrondtheorieën beschrijven wiskundige en datastructuureigenschappen zoals lineaire aritmetiek over de reële of gehele getallen, arrays, bitvectoren en oninterpreteerde functies. SMT-problemen worden doorgaans ingevoerd in de SMT-LIB-standaard en zijn bedoeld voor automatische satisfiability-checks van formules.

In de gebruikelijke aanpak wordt de booleaanse structuur van de formule behandeld door een SAT-solver, terwijl theorie-solveren de mogelijkheden van de achtergrondtheorie controleren, conflicten melden en theorielemmas genereren. De twee niveaus wisselen informatie uit via theorielemmas en conflictrapportages, waardoor een efficiënt zoekproces ontstaat. De gangbare architectuur wordt DPLL(T) genoemd.

Veelvoorkomende theorieën zijn lineaire aritmetiek over reële of gehele getallen, arrays, bitvectoren en oninterpreteerde functies. Sommige theorieën zijn afzonderlijk beslisbaar; de combinatie van theorieën vereist vaak techniek zoals Nelson-Oppen. Het toevoegen van kwantificatie maakt het oplossen ingewikkelder en kan leiden tot onvolledige procedures; in de praktijk worden heuristische instantiërings- en modelgebaseerde methoden gebruikt.

Toepassingen omvatten software- en hardwareverificatie, formele verificatie, foutopsporing in compilers en beveiligingsanalyse. SMT-tools leveren vaak modellen of tegenvoorbeelden als een formule onhaalbaar blijkt.

Bekende SMT-tools zijn Z3, CVC4/CVC5, Yices en MathSAT. SMT wordt vastgelegd in de SMT-LIB-standaard, die invoer- en theorie-definities specificeert en interoperabiliteit ondersteunt. Uitdagingen blijven onder meer niet-lineaire aritmetiek, het gebruik van kwantoren en de efficiënte combinatie van meerdere theorieën.