Límites de los solucionadores SMT

Question

Tradicionalmente, la mayoría de los trabajos con lógica computacional eran proposicionales, en cuyo caso se utilizaba un solucionador SAT (boolean satisfiability) o de primer orden, en cuyo caso se usaba un teorema de primer orden.

En los últimos años, se han realizado muchos progresos en la resolución de SMT (Teoría del módulo de satisfacibilidad), que básicamente aumentan la lógica proposicional con las teorías de la aritmética, etc .; John Rushby de SRI International llega a llamarlos una tecnología disruptiva.

¿Cuáles son los ejemplos prácticos más importantes de problemas que se pueden manejar en la lógica de primer orden pero que aún no pueden ser manejados por SMT? Más particularmente, ¿qué tipo de problemas surgen que no pueden ser manejados por SMT en el dominio de la verificación de software?

Answer 1

Los solucionadores de SMT no son más potentes que los solucionadores de SAT. Todavía se ejecutarán en tiempo exponencial o estarán incompletos por los mismos problemas en SAT. La ventaja de SMT es que muchas cosas que son obvias en SMT pueden tardar mucho tiempo en redescubrir un solucionador sat equivalente.

De modo que con la verificación del software como ejemplo, si utiliza un solucionador SMT QF BV (teoría de los vectores de bits sin cuantificador), el solucionador SMT sabrá que (a + b = b + a) en una palabra nivel en cambio, mientras que a un solucionador de SAT le puede tomar mucho tiempo demostrar que usa los valores booleanos individuales.

Por lo tanto, para la verificación del software, puede fácilmente crear problemas en la verificación del software que serían difíciles para cualquier solucionador de SMT o SAT.

En primer lugar, los bucles deben desenrollarse en QF BV, lo que significa que prácticamente debe limitar lo que el solucionador busca. Si se permitieron los cuantificadores, se convierte en un problema completo de PSPACE, no solo en NP-completo.

En segundo lugar, los problemas que se consideran difíciles en general son fáciles de codificar en QF BV. Por ejemplo, se puede escribir un programa de la siguiente manera:

void run(int64_t a,int64_t b) 
{ 
    a * b == <some large semiprime>; 

    assert (false); 
} 

Ahora, por supuesto, el solucionador SMT resultará fácilmente que afirman (falso) se producirá, pero tendrá que proporcionar un contraejemplo, que le dará la entradas a,b. Si configura <some large number> en una semiprima RSA, entonces simplemente invirtió la multiplicación ... ¡también conocida como factorización de enteros! Por lo tanto, esto será difícil para cualquier solucionador de SMT, y demuestra que la verificación de software es un problema difícil en general (a menos que P = NP, o al menos la factorización de enteros se vuelva fácil). Tales solucionadores de SMT son una ventaja para los solucionadores de SAT al vestir las cosas en un lenguaje más fácil de escribir y más fácil de razonar.

Los solucionadores SMT que resuelven teorías más avanzadas son necesariamente incompletos o incluso más lentos que los solucionadores de SAT, porque están intentando resolver problemas más difíciles.

Consulte también:

• Curiosamente, el Beaver SMT solver traduce QF BV a CNF y puede utilizar un solucionador SAT como un back-end.
• Klee que puede llevar un programa compilado a LLVM IR (representación intermedia), y busca errores, y encuentra ejemplos de contador para aserciones, etc. Si encuentra un error, puede dar un contraejemplo a la corrección (lo hará darle información que reproducirá el error).