performance - Z3 aritmética real y estadística

encoding statistics

Question

Dado un problema que está codificado usando los reales de Z3, ¿cuál de las estadísticas que produce Z3 /smt2 /st podría ser útil para juzgar si el motor real "tiene problemas / hace mucho trabajo"?

En mi caso, tengo dos codificaciones del problema en su mayoría equivalentes, ambas usando reales. La "pequeña" diferencia en la codificación, sin embargo, hace una gran diferencia en el tiempo de ejecución, es decir, que la codificación A tarda 2: 30min y la codificación B 13min. Las estadísticas Z3 muestran que los conflicts y quant-instantiations son en su mayoría equivalentes, pero otros no son, por ejemplo, grobner , pivots y nonlinear-horner .

Las dos estadísticas diferentes están disponibles como una esencia .

EDITAR (para abordar el comentario de Leo):

La codificación SMT2 generada por ambas versiones es ~ 30k líneas y las aserciones donde se usan los reales se rocían por todo el código. La diferencia principal es que la codificación B usa muchas constantes de tipo real no especificadas del rango de 0.0 a 1.0 que están limitadas por desigualdades, por ejemplo, 0.0 < r1 < 1.0 o 0.0 < r3 < 0.75 - r1 - r2 , mientras que en la codificación A muchos estas constantes no especificadas han sido reemplazadas por valores reales fijos del mismo rango, por ejemplo, 0.1 o 0.75 - 0.01 . Ambas codificaciones usan aritmética real no lineal, por ejemplo, r1 * (1.0 - r2) .

Algunos ejemplos aleatorios de las dos codificaciones están disponibles como esencia . Todas las variables que ocurren son reales no especificados como se describió anteriormente.

PD: ¿Introducir alias para valores reales fijos, por ejemplo,

(define-sort $Perms () Real)
(declare-const $Perms.$Full $Perms)
(declare-const $Perms.$None $Perms)
(assert (= $Perms.Zero 0.0))
(assert (= $Perms.Write 1.0))

infligir sanciones de rendimiento significativo?

Answer 1

El nuevo solucionador aritmético no lineal solo se usa en problemas que solo contienen aritmética. Como su problema usa cuantificadores, no se usará el nuevo solucionador no lineal. Por lo tanto, Z3 usará el viejo enfoque basado en una combinación de: Simplex (pivots stat), Groebner Basis (groebner stat), y Propagación de intervalos (horner stat). Este no es un método completo. Además, en base a los fragmentos que publicaste en esencia, la base de Groebner no será muy efectiva. Este método generalmente es efectivo en problemas que contienen muchas igualdades. Por lo tanto, es probable que sea solo por encima. Puede desactivarlo usando la opción NL_ARITH_GB=false . Por supuesto, esto es solo una suposición basada en el fragmento de problema que publicaste.

Las diferencias entre la codificación A y B son sustanciales. La codificación A es esencialmente un problema lineal, ya que varias constantes se fijaron a valores reales. Z3 siempre fue completo para problemas aritméticos lineales. Entonces, esto debería explicar la diferencia en el rendimiento.

En cuanto a su pregunta sobre alias, la forma preferida de introducir alias es:

(define-const $Perms.$Zero $Perms 0.0)
(define-const $Perms.$Write $Perms 1.0)

Z3 también contiene un preprocesador que elimina variables usando ecuaciones lineales. Este preprocesador está deshabilitado por defecto en problemas que contienen cuantificadores. Esta decisión de diseño está motivada por herramientas de verificación de programas que hacen un uso extensivo de desencadenantes / patrones en cuantificadores. El proceso de eliminación variable puede modificar los desencadenantes / patrones cuidadosamente diseñados y afectar el tiempo de ejecución total. Puede usar la nueva táctica / marco de estrategia en Z3 para forzarlo a aplicar este preprocesador. Puedes reemplazar el comando

(check-sat)

con

(check-sat-using (then simplify solve-eqs smt))

Esta estrategia le indica a Z3 que ejecute el simplificador, luego resuelva las ecuaciones (y elimine las variables) y luego ejecute el motor de solución predeterminada smt . Puede encontrar más sobre tácticas y estrategias en el siguiente tutorial .