Comprender el rendimiento de los solucionadores QFBV SMT

Los solucionadores SMT como Z3 o Boolector utilizan un conjunto complejo de heurísticas para resolver problemas. Sin embargo, esto también hace que sea muy difícil predecir el rendimiento de un solucionador de este tipo para un problema dado. Mi pregunta es así:

Pregunta

¿Hay alguna manera de comprender u obtener información sobre el rendimiento de un solucionador SMT para un específico en la teoría de los vectores de bits libres de cuantificador (QFBV)?

Esto también incluye cualquier herramienta de visualización que ayudaría a comprender dónde está "atascado" el solucionador / no progresa.

Aplicaciones

• Comprenda de antemano cómo las diferentes codificaciones del mismo problema afectan el rendimiento del solucionador (el estado del arte aquí no puede ser "solo pruebe algunas codificaciones diferentes y espere que una sea lo suficientemente rápida", ¿verdad?)

• Si un solucionador SMT no puede resolver un problema dado debido a limitaciones de tiempo, encuentre una manera de expresar el problema de manera diferente para que pueda resolverse.

• Evite perder tiempo en simplificaciones de problemas específicos del dominio que no afectarán en absoluto el rendimiento del solucionador o incluso afectarán negativamente el rendimiento del solucionador.

Investigación existente

Traté de encontrar investigaciones sobre este tema, pero no he podido encontrar mucho. Todavía no tengo mucha experiencia en el campo de los solucionadores SAT / SMT, por lo que me disculpo si me he perdido algo.

• SATzilla : predice el mejor solucionador basado en características extraídas del problema utilizando técnicas de aprendizaje automático.

  Esto se aplica solo con SAT en lugar de SMT, y no explica los motivos del rendimiento de los solucionadores.

• Perfilador de axioma Z3 Una visualización del gráfico de instanciación Z3 y análisis de bucles coincidentes

  Parece que esto se centra solo en las teorías cuantificadas.

La respuesta corta es no, no la entendemos. La respuesta larga es sí, tenemos algunos límites, pero esos límites no son muy útiles. Está bastante claro que el peor tiempo de ejecución es exponencial. Eso no es muy útil, porque sabemos que en algunas / muchas situaciones prácticas, parece funcionar bastante rápido, y realmente no sabemos por qué.

No sabemos por qué eso es cierto para los solucionadores de SAT, y mucho menos para QFBV. Comprender por qué los solucionadores de QFBV a menudo son rápidos parece al menos tan difícil como comprender por qué los solucionadores de SAT a menudo son rápidos, lo que ya está más allá de nuestro nivel actual de comprensión. Si busca más en este sitio, puede encontrar un resumen de los intentos actuales de comprender el último tema.