Problema satisfacabilității formulelor în teorii

Versiunea actuală a paginii nu a fost încă revizuită de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 15 ianuarie 2019; verificările necesită 2 modificări .

Problema satisfacabilității formulelor în teorii ( în engleză satisfiability modulo theories , SMT) este problema solubilității formulelor logice, ținând cont de teoriile care stau la baza acestora. Exemple de astfel de teorii pentru formulele SMT sunt: teorii ale numerelor întregi și ale numerelor reale, teorii ale listelor, tablourilor, vectorilor de biți etc.

Concepte de bază

Formal , o formulă SMT este o formulă în logica de ordinul întâi în care unele funcții și simboluri predicate au o interpretare suplimentară. Sarcina este de a determina dacă formula dată este fezabilă. Cu alte cuvinte, spre deosebire de problema de satisfacție pentru formulele booleene , în loc de variabile booleene, formula SMT conține variabile arbitrare, iar predicatele sunt funcții booleene ale acestor variabile.

Exemple de predicate sunt inegalitățile liniare ( ) sau egalitățile care implică așa-numiții termeni neinterpretați sau simboluri de funcție : , unde este o funcție nedefinită a două argumente. Predicatele sunt interpretate în funcție de teoria căreia îi aparțin. De exemplu, inegalitățile liniare asupra variabilelor reale sunt evaluate conform regulilor teoriei aritmeticii reale liniare, în timp ce predicatele peste termeni neinterpretați și simbolurile funcției sunt evaluate conform regulilor teoriei funcțiilor neinterpretate cu egalitate (numită și teorie goală). . SMT include, de asemenea, teorii ale matricelor și listelor (folosite adesea pentru modelarea și verificarea programelor ) și teoria vectorului de biți (folosită adesea pentru modelarea și verificarea hardware). Sunt posibile și subteorii: de exemplu, logica diferențelor este o subteorie a aritmeticii liniare, în care inegalitățile sunt limitate la următoarea formă pentru variabilele și și constanta . $3x+2y-z\geqslant 4$ $f(f(u,v),v)=f(u,v)$ $f$ $xy\leq c$ $X$ $y$ $c$

Majoritatea soluțiilor SMT acceptă numai formule non-cuantificatoare .

Puterea expresivă a SMT

Formula SMT este o generalizare a formulei booleene SAT în care variabilele sunt înlocuite cu predicate din teoriile relevante. Prin urmare, SMT-urile oferă mai multe opțiuni de modelare decât formulele SAT. De exemplu, formula SMT vă permite să modelați operațiile unei funcții ale modulelor de microprocesor la nivel de cuvânt , mai degrabă decât la nivel de biți .

Rezolvatori SMT

Primele încercări de a rezolva problemele SMT au vizat conversia acestora în formule SAT (de exemplu, variabilele de 32 de biți au fost codificate cu 32 de variabile booleene care codifică operațiile corespunzătoare pe cuvinte în operații de nivel scăzut pe biți) și rezolvarea formulei SAT cu o rezolvator. Această abordare are avantajele sale - vă permite să utilizați soluții SAT existente fără modificări și să utilizați optimizările făcute în acestea. Pe de altă parte, pierderea semanticii de nivel înalt a teoriilor subiacente înseamnă că rezolvatorul SAT trebuie să facă eforturi mari pentru a deduce fapte „evidente” (cum ar fi pentru adunare). Această considerație a condus la rezolvatori SMT specializați care integrează dovezi booleene convenționale în stil DPLL cu soluții specifice teoriei ( T-solvers ) care funcționează cu disjuncții și conjuncții de predicate dintr-o anumită teorie. $x+y=y+x$

Arhitectura DPLL(T) transferă funcțiile de demonstrație booleene către solutorul SAT, care la rândul său interacționează cu rezolvatorul teoriei T. Rezolvatorul SAT generează modele în care unele dintre literalele care intră fără negație nu sunt variabile booleene, ci instrucțiuni atomice. a unora, posibil multisortate, teorie de ordinul întâi. Rezolvatorul de teorie încearcă să găsească inconsecvențe în modelele transmise acestuia, iar dacă nu se găsește o astfel de inconsecvență, formula este declarată satisfăcătoare. Pentru ca această integrare să funcționeze, rezolvatorul de teorie trebuie să participe la analiza conflictului oferind explicații pentru infezabilitatea atunci când apar conflicte, care sunt stocate în soluție pe baza arhitecturii DPLL. Deoarece numărul modelelor SAT este finit, enumerarea va conduce la un răspuns în timp finit [1] .

Rezolvatori acceptați și dezvoltați activ: Alt-Ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, MathSAT, OpenSMT, SateEEn, Spear, STP, UCLID, veriT, Yices, Z3.
Altele: Argo-lib, Ario, CVC, CVC Lite, Fx7, haRVey, HTP, ICS, LPSAT, RDL, Sammy, Simplify, Simplics, STeP, SVC, Tsat++.

Note

↑ 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, 7-9 decembrie 2011. Proceedings. DOI 10.1007/978-3-642-25379-9_12

Literatură

Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. Rezolvarea SAT și SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL( T ) // Journal of the ACM. - 2006. - T. 53 , nr 6 . - P. 937-977.
Biere, A. și Gomes, CP Theory and Applications of Satisfiability Testing - SAT 2006: a 9th International Conference, Seattle, WA, SUA, 12-15 august 2006, Proceedings . — Springer, 2006. — P. 142-155 . — 438 p. — ISBN 9783540372066 .
D.Yurichev, Introducere rapidă în solutoarele SAT/SMT și execuția simbolică