DPLL(T)

Algoritmo para resolver problemas SMT

En informática, DPLL(T) es un marco para determinar la satisfacibilidad de los problemas SMT . El algoritmo extiende el algoritmo DPLL original de resolución de SAT con la capacidad de razonar sobre una teoría arbitraria T. ^{[1] [2] [3]} En un nivel alto, el algoritmo funciona transformando un problema SMT en una fórmula SAT donde los átomos se reemplazan con variables booleanas. El algoritmo encuentra repetidamente una valoración satisfactoria para el problema SAT, consulta un solucionador de teoría para verificar la consistencia bajo la teoría específica del dominio y luego (si se encuentra una contradicción) refina la fórmula SAT con esta información. ^[4]

Muchos solucionadores SMT modernos, como Z3 Theorem Prover y CVC4 de Microsoft , utilizan DPLL(T) para potenciar sus capacidades de resolución principales. ^{[5] [6] [7]}

Referencias

1. Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). "DPLL(T): Fast Decision Procedures". En Alur, Rajeev; Peled, Doron A. (eds.). Verificación asistida por computadora . Apuntes de clase en informática. Vol. 3114. Springer Berlin Heidelberg. págs. 175–188. doi : 10.1007/978-3-540-27813-9_14 . ISBN . 9783540278139.
2. Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2006). "Resolución de las teorías SAT y SAT módulo: desde un procedimiento abstracto Davis–Putnam–Logemann–Loveland hasta DPLL(T)". J. ACM . 53 (6): 937–977. doi :10.1145/1217856.1217859. ISSN  0004-5411. S2CID  14058631.
3. Nieuwenhuis, Robert; Oliveras, Albert (2005). "DPLL(T) con propagación exhaustiva de teorías y su aplicación a la lógica diferencial". En Etessami, Kousha; Rajamani, Sriram K. (eds.). Verificación asistida por computadora . Apuntes de clase en informática. Vol. 3576. Springer Berlin Heidelberg. págs. 321–334. doi : 10.1007/11513988_33 . ISBN. 9783540316862.
4. Reynolds, Andrew (2015). "Teorías del módulo de satisfacibilidad y DPLL(T)" (PDF) . The University of Iowa . Consultado el 8 de abril de 2019 .
5. de Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: Un solucionador SMT eficiente". En Ramakrishnan, CR; Rehof, Jakob (eds.). Herramientas y algoritmos para la construcción y análisis de sistemas . Apuntes de clase en informática. Vol. 4963. Springer Berlin Heidelberg. págs. 337–340. doi : 10.1007/978-3-540-78800-3_24 . ISBN . 9783540788003.
6. Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "Un solucionador de teoría DPLL(T) para una teoría de cadenas y expresiones regulares". En Biere, Armin; Bloem, Roderick (eds.). Verificación asistida por computadora . Apuntes de clase en informática. Cham: Springer International Publishing. págs. 646–662. doi : 10.1007/978-3-319-08867-9_43 . ISBN . 978-3-319-08867-9.
7. Bruttomesso, Roberto; Cimatti, Alessandro; Franzen, Anders; Grigio, Alberto; Sebastiani, Roberto (2008). "El solucionador SMT MathSAT 4". En Gupta, Aarti ; Malik, Sharad (eds.). Verificación asistida por computadora . Apuntes de conferencias sobre informática. vol. 5123. Springer Berlín Heidelberg. págs. 299–303. doi : 10.1007/978-3-540-70545-1_28 . ISBN 9783540705451.