SMT solver es un procedimiento de resolución de SAT + decisión
Un solucionador SAT es un solucionador para un problema de decisión: el problema SAT es un problema de decisión. Además, este problema de decisión es "auto reducible":
El problema SAT es auto-reducible, es decir, cada algoritmo que responde correctamente si una instancia de SAT es solucionable puede usarse para encontrar una asignación satisfactoria
- ( wikipedia )
Esto significa que los solucionadores de SAT también pueden dar la tarea satisfactoria, además de decidir el problema.
Los solucionadores TL; DR SMT resuelven una generalización del problema SAT, dependiendo de los tipos / restricciones permitidos en la teoría. Además, también permiten la codificación de relaciones de tipo de nivel superior a las permitidas por las codificaciones SAT.
Un solucionador SAT generalmente se ocupa de muchas variables booleanas individuales, que están relacionadas solo a través de las cláusulas / restricciones del CNF . Un solucionador SMT de la teoría QF_BV (vector de bits sin cuantificador) es básicamente un solucionador SAT + más información sobre las relaciones. Por ejemplo, un solucionador QF_BV SMT es reducible a SAT 1 . Entonces, ¿por qué usar un solucionador QF_BF SMT? La principal ventaja es que en SAT, un entero está representado por diferentes variables, que a primera vista pueden parecer no relacionadas. Un solucionador SAT pasaría mucho tiempo reaprendiendo relaciones simples, como en un nivel entero( A = B ) ∧ ( B = C)⟹( A = C) , mientras que el solucionador SMT sabe que los bits individuales están relacionados de esta manera desde el principio, porque el lenguaje QF_BV SMT está en un nivel entero (ancho de bits fijo). Por lo tanto, un solucionador QF_BV SMT puede razonar en el nivel entero, además del nivel de bit.
- Vea Beaver SMT solucionador que incluso puede generar el problema SAT equivalente que necesitaría ser resuelto.
Si bien el solucionador QF_BV SMT tiene esta ventaja sobre un solucionador SAT, no creo que sea una ventaja de complejidad: ambos son esencialmente equivalentes y toman un tiempo exponencial para resolver sus peores problemas. Pero prácticamente, un solucionador QF_BV SMT podría ser mucho más rápido debido a este conocimiento adicional. Vea mi respuesta a Límites de solucionadores SMT , para ver un ejemplo de algo considerado "difícil" que los solucionadores QF_BV SMT (actuales) y los solucionadores SAT se ahogarían.
También hay solucionadores SMT que intentan resolver problemas aún más difíciles que la Satisfacción booleana (por ejemplo, permitiendo tipos y restricciones en reales, o permitiendo cuantificadores); obviamente, estos son teóricamente al menos tan lentos como un solucionador SAT. Estos solucionadores SMT están resolviendo una generalización del problema SAT; en lugar de usar variables binarias, cada "teoría" permite relaciones / restricciones sobre diferentes dominios, como reales, o restricciones cuantificadas (para todos).
Prover teorema
Un comprobador de teoremas automatizado es un solucionador que, dado algún tipo de sistema de prueba, algunos supuestos y un objetivo para demostrar, "llenará los espacios" entre los supuestos y el objetivo. También tendrá algún tipo de verificador para verificar las pruebas (que se ejecuta rápidamente). Un probador de teoremas puede confiar en un solucionador SAT para completar los espacios en blanco; de hecho, si y hay un algoritmo práctico para resolver problemas NP-completos, uno puede probar casi todas las cosas útiles comprobables (en un tiempo razonable):PAGS= NPAGS
Pero tales cambios pueden tener una importancia insignificante en comparación con la revolución que un método eficiente para resolver problemas NP-completos causaría en las matemáticas mismas. Según Stephen Cook, [19]
... transformaría las matemáticas al permitir que una computadora encuentre una prueba formal de cualquier teorema que tenga una prueba de una longitud razonable, ya que las pruebas formales pueden reconocerse fácilmente en el tiempo polinómico. Los problemas de ejemplo pueden incluir todos los problemas del premio CMI.
- ( wikipedia )
[19]: Cook, Stephen (abril de 2000). El problema P versus NP. Instituto de Matemáticas Clay (PDF) .
La razón por la que esto funcionaría es porque "las pruebas formales se pueden reconocer fácilmente en tiempo polinomial" a través del verificador, y implicaría que los problemas que se pueden verificar en tiempo polinomial también se pueden responder en tiempo polinomial.PAGS= NPAGS
Pero por ahora, el teorema automatizado en su mayoría prueba el uso de algoritmos heurísticos o exponenciales de tiempo (pero aún son útiles).
Solucionador de restricciones
Estas suelen ser reformulaciones de los solucionadores SAT / SMT en otros idiomas. Si alguna vez usó algún solucionador SAT / SMT para resolver un problema, realmente puede llegar a amar la capacidad no determinista de los solucionadores. Es decir, en lugar de decirle a la computadora cómo hacer algo, le dices lo que quieres , es decir. qué propiedades desea que tenga la salida, y un solucionador SAT / SMT lo "rellenará" de manera no determinista, sin molestarlo con los detalles de implementación. Este tipo de paradigma de programación es muy atractivo y se llama programación de restricciones , y para ejecutarse, debe usar un solucionador de restricciones (que podría usar un solucionador SAT / SMT en el back-end, dependiendo de los tipos y restricciones que le permite usar) .
Pero veo personas que llaman a Z3 un probador de teoremas. Entonces no sé cómo distinguir esos términos.
AFAIK, Z3 es un conjunto de muchas herramientas, que incluyen un solucionador SMT, varios lenguajes de comprobación de teoremas / modelos y más.
¿Y cuál es el término más general para todos ellos?
Creo que la generalización del problema de la satisfacción son las Teorías del módulo de satisfacción , por lo que "SMT solucionador" sería la más general de todas estas. Sin embargo, no todas las implementaciones reales de solucionador SMT resuelven todas las teorías, por lo que esto no significa que todos los solucionadores SMT sean igualmente generales.
