pura - ¿Cómo maneja Z3 la aritmética de enteros no lineales?
programacion entera pura (1)
Soy consciente de que la teoría de los enteros con la multiplicación es genéricamente indecidible. Sin embargo, en ciertos casos, Z3 devuelve un modelo. Tengo curiosidad por saber cómo se hace esto. ¿Tiene algo que ver con el nuevo procedimiento de decisión para la aritmética no lineal sobre los reales? ¿Qué instancias específicas (por ej .: enteros bajo módulo finito, etc.) han sido reconocidas para las cuales Z3 devuelve un modelo para una consulta de multiplicación? Cualquier ayuda es muy apreciada.
Sí, el problema de decisión para la aritmética de enteros no lineales es indecidible. Podemos codificar el problema de Detención para máquinas de Turing en la aritmética de enteros no lineales. Recomiendo encarecidamente el hermoso libro del décimo problema de Hilbert para cualquiera que esté interesado en este problema.
Tenga en cuenta que, si una fórmula tiene una solución, siempre podemos encontrarla por fuerza bruta. Es decir, seguimos enumerando todas las asignaciones posibles y probando si satisfacen la fórmula o no. Esto no es tan diferente de tratar de resolver el problema de Detención simplemente ejecutando el programa y verificando si termina después de un número dado de pasos.
Z3 no realiza una enumeración ingenua. Dado un número k , codifica todas las variables enteras usando k bits y reduce todo a la lógica proposicional. Entonces, se usa un solucionador de SAT para encontrar una solución. Si se encuentra una solución, la convierte de nuevo en una solución entera para la fórmula original. Si no hay una solución para el Propositional formal, entonces intenta aumentar k , o cambia a una estrategia diferente. Esta reducción a la lógica proposicional es esencialmente un procedimiento de búsqueda de modelo / solución. No puede mostrar que un problema no tiene una solución. En realidad, para problemas donde cada variable entera tiene un límite inferior y superior, puede hacerlo. Entonces, Z3 tiene que usar otras estrategias para demostrar que no existe una solución.
Además, la reducción a la lógica Propositional solo funciona si hay una solución muy pequeña (una solución que necesita un pequeño número de bits para codificar). Lo discuto en la siguiente publicación:
Z3 no tiene un buen soporte para la aritmética de enteros no lineales. El enfoque descrito anteriormente es muy simplista. En mi opinión, Mathematica parece tener la cartera más completa de técnicas:
http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems
Finalmente, el solucionador aritmético real no lineal (NLSat) no se usa por defecto para problemas de enteros no lineales. Por lo general, es muy ineficaz en problemas enteros. No obstante, podemos forzar a Z3 a usar NLSat incluso para problemas enteros. Solo tenemos que reemplazar:
(check-sat)
Con
(check-sat-using qfnra-nlsat)
Cuando se usa este comando, Z3 resolverá el problema como un problema real. Si no se encuentra una solución real, sabemos que no hay una solución entera. Si se encuentra una solución, Z3 verificará si la solución realmente está asignando valores enteros a las variables enteras. Si ese no es el caso, regresará unknown para indicar que no pudo resolver el problema.