TryFor en Z3 no deja de verificar después del límite de tiempo dado

Question

Estoy usando la API .NET de Z3. Cuando una instancia de un solucionador llamando:

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit)); 

y darle un TimeLimit de 60 segundos (60000 milisegundos) para algunos modelos de la declaración

s.Check() 

no vuelve después de 60 segundos. Para algunos modelos, regresa unos segundos más tarde, lo que en mi caso no sería un problema, pero para algunos modelos no se devuelve (cancelé el proceso después de 3 días).

¿Cómo puedo forzar a Z3 a dejar de verificar después de un límite de tiempo determinado?

Answer 1

El combinador TryFor se implementa utilizando una bandera de "cancelación". Las nuevas tácticas son muy receptivas y terminan muy rápidamente cuando se establece la bandera de "cancelación". Desafortunadamente, la táctica de propósito general smt es una envoltura sobre un solucionador de propósito general. Este solucionador de propósito general no es muy receptivo. Se puede "perder" en varios lugares clave: instanciación de cuantificadores, Simplex, etc. La táctica qflia se basa en el smt y muchas otras tácticas. Desde entonces, estás tratando de resolver problemas sin cuantificadores. Supongo que la táctica smt está en un bucle dentro del módulo Simplex. El módulo Simplex en la táctica smt se implementa utilizando números racionales de precisión arbitraria. Por lo tanto, puede llevar mucho tiempo para problemas lineales/enteros no triviales.

No hay mucho que pueda hacer para solucionar este problema. Si realmente necesita una gran garantía en el tiempo de ejecución, la única solución que veo es crear un proceso separado ejecutando Z3, y matarlo cada vez que se necesita más k segundos para resolver un problema.

Dicho esto, las futuras versiones de Z3 tendrán un nuevo módulo aritmético completo. Este nuevo módulo (como las nuevas tácticas) terminará rápidamente cuando se establece el indicador de cancelación.