Intento usar el solucionador z3 para un problema de minimización. Estaba tratando de obtener un tiempo de espera y devolver la mejor solución hasta ahora. Uso la API de Python y la opción de tiempo de espera "smt.timeout" con

set_option("smt.timeout", 1000) # 1s timeout

Esto realmente se agota después de aproximadamente 1 segundo. Sin embargo, un tiempo de espera mayor no proporciona un objetivo menor. Terminé encendiendo la verbosidad con

set_option("verbose", 2)

Y creo que z3 evalúa sucesivamente valores más grandes de mi objetivo, hasta que el problema sea satisfactorio:

(opt.maxres [0:6117664])
(opt.maxres [175560:6117664])
(opt.maxres [236460:6117664])
(opt.maxres [297360:6117664])
...
(opt.maxres [940415:6117664])
(opt.maxres [945805:6117664])
...

Por lo tanto, tengo las dos preguntas:

Por el contrario, ¿puedo decirle a z3 que comience con el límite superior y que devuelva sucesivamente modelos con un valor más pequeño para mi función objetivo (como, por ejemplo, las anotaciones de Minizincindomain_max http://www.minizinc.org/2.0/doc-lib/doc-annotations-search.html)Todavía parece que el solucionador devuelve una instancia satisfactoria de mi problema. ¿Cómo se encuentra? Si está tratando de evaluar sucesivamente valores más grandes de mi objetivo, aún no debería haber encontrado una instancia satisfactoria cuando se produce el tiempo de espera ...

editar: En el registro opt.maxres, el límite superior nunca se contrae.

Para el registro, encontré una descripción más detallada de las opciones en la fuente aquíopt_params.pyg

Editar Lamento molestar, he empezado a sumergirme en esto recientemente una vez más. De todos modos, creo que esto podría ser útil para otros. He estado descubriendo que en realidad tengo que llamar alOptimize.upper para obtener el límite superior, y el modelo todavía no es el que corresponde a este límite superior. He podido agregarlo como una nueva restricción y llamar a un solucionador (sin optimización, solo SAT), pero probablemente esa no sea la mejor idea. Leyendoesta Siento que debería llamarOptimize.update_upper después del tiempo de espera del solucionador, pero la interfaz de Python no tiene dicho método (?). Al menos puedo obtener el límite superior y el modelo correspondiente ahora (a costa de cálculos innecesarios, supongo).