tactil - xperia z3 compact review

¿Cómo funciona la solución incremental en Z3?

Question

Tengo una pregunta sobre cómo Z3 resuelve problemas de forma incremental. Después de leer algunas respuestas aquí, encontré lo siguiente:

1. Hay dos formas de usar Z3 para la resolución incremental: una es el modo push / pop (stack), la otra usa suposiciones. Restricciones suaves / duras en Z3 .
2. En el modo de pila, z3 olvidará todos los lemas aprendidos en el alcance global (¿ estoy en lo cierto? ) Incluso después de un "pop" local. Eficiencia de fortalecimiento de restricciones en solucionadores de SMT
3. En el modo de suposiciones (no sé el nombre, ese es el nombre que se me viene a la mente), z3 no simplificará algunas fórmulas, por ejemplo, la propagación de valores. Comportamiento de z3 cambiando a petición para unsat core

Hice algunas comparaciones (pueden pedir las fórmulas, son demasiado grandes para ponerlas en rise4fun), pero estas son mis observaciones: en algunas fórmulas, incluidos los cuantificadores, el modo de suposiciones es más rápido. En algunas fórmulas con muchas variables booleanas (variables de suposiciones), el modo de pila es más rápido que el modo de suposiciones.

¿Se implementan para fines específicos? ¿Cómo funciona la solución incremental en Z3?

Answer 1

Sí, hay esencialmente dos modos incrementales.

Basado en pila: usando push (), pop () crea un contexto local, que sigue una disciplina de pila. Las afirmaciones agregadas bajo un push () se eliminan después de un pop coincidente (). Además, se eliminan todos los lemmas derivados de un empuje. Use push () / pop () para emular la congelación de un estado y agregar restricciones adicionales sobre el estado congelado, luego reanude el estado congelado. Tiene la ventaja de que se libera cualquier sobrecarga de memoria adicional (como lemas aprendidos) acumulada dentro del alcance de un push (). El supuesto de trabajo es que los lemas aprendidos bajo un impulso ya no serían útiles.

Basada en la suposición: utilizando literales de suposición adicionales pasados ​​a check () / check_sat () puede (1) extraer núcleos insatisfactorios sobre los literales de asunción, (2) ganar incrementalidad local sin lemas recolectores de basura que se derivan independientemente de las suposiciones. En otras palabras, si Z3 aprende un lema que no contiene ninguno de los literales de suposición, espera que no los recoja. Para utilizar los literales de suposición de manera efectiva, también debería agregarlos a las fórmulas. Entonces la compensación es que las cláusulas usadas con suposiciones contienen cierta cantidad de hinchazón. Por ejemplo, si desea asumir localmente alguna fórmula (<= xy), entonces agrega una cláusula (=> p (<= xy)), y asuma p cuando llame a check_sat (). Tenga en cuenta que la suposición original era una unidad. Z3 propaga las unidades de manera eficiente. Con la formulación que usa literales de suposición, ya no es una unidad en el nivel básico de búsqueda. Esto genera un gasto extra. Las unidades se convierten en cláusulas binarias, las cláusulas binarias se convierten en cláusulas ternarias, etc.

La diferenciación entre la funcionalidad push / pop se mantiene para el motor SMT predeterminado de Z3. Este es el motor que usarán la mayoría de las fórmulas. Z3 contiene una cartera de motores. Por ejemplo, para problemas de vector de bits puros, Z3 puede terminar usando el motor basado en sat. La incrementalidad en el motor basado en sat se implementa de forma diferente al motor predeterminado. Aquí la incrementalidad se implementa usando supuestos literales. Cualquier aserción que agregue dentro del alcance de un empuje se afirma como una implicación (=> fórmula scope_literals). check_sat () dentro de dicho ámbito tendrá que ocuparse de los literales de asunción. Por otro lado, cualquier consecuencia (lema) que no dependa del alcance actual no es basura recolectada en pop ().

En el modo de optimización, cuando afirma los objetivos de optimización o cuando utiliza los objetos de optimización en la API, también puede invocar push / pop. Del mismo modo con puntos fijos. Para estas dos características, push / pop son esencialmente para la conveniencia del usuario. No hay incrementalidad interna. La razón es que estos dos modos usan preprocesamiento sustancial que es súper no incremental.