Comprendre les performances des solveurs QFBV SMT

Les solveurs SMT tels que Z3 ou Boolector utilisent un ensemble complexe d'heuristiques pour résoudre les problèmes. Cependant, cela rend également très difficile la prévision des performances d'un tel solveur pour un problème donné. Ma question est donc:

Question

Existe-t-il un moyen de comprendre ou d'obtenir des informations sur les performances d'un solveur SMT pour un spécifique de la théorie des vecteurs binaires sans quantificateur (QFBV)?

Cela inclut également tous les outils de visualisation qui pourraient aider à comprendre où le solveur est «bloqué» / ne progresse pas.

Applications

• Comprendre à l'avance comment différents encodages du même problème affectent les performances du solveur (l'état de l'art ici ne peut pas être "essayez simplement quelques encodages différents et espérez que l'un est assez rapide", non?)

• Si un problème donné ne peut pas être résolu par un solveur SMT en raison de contraintes de temps, trouvez un moyen d'exprimer le problème différemment afin qu'il puisse être résolu.

• Évitez de perdre du temps sur des simplifications de problèmes spécifiques au domaine qui n'affecteront pas du tout les performances du solveur, ni même les performances du solveur

Recherche existante

J'ai essayé de trouver des recherches sur ce sujet, mais je n'ai pas pu trouver grand chose. Je n'ai pas encore beaucoup d'expérience dans le domaine des solveurs SAT / SMT, donc je m'excuse si j'ai raté quelque chose.

• SATzilla : prédit le solveur le plus performant en fonction des fonctionnalités extraites du problème à l'aide de techniques d'apprentissage automatique.

  Cela s'applique uniquement avec SAT au lieu de SMT et n'explique pas les raisons des performances des solveurs.

• Profileur d'axiome Z3 Visualisation du graphique d'instanciation Z3 et analyse des boucles correspondantes

  On dirait que cela se concentre uniquement sur les théories quantifiées.

La réponse courte est non, nous ne la comprenons pas. La réponse longue est oui, nous avons des limites, mais ces limites ne sont pas très utiles. Il est tout à fait clair que le temps d'exécution le plus défavorable est exponentiel. Ce n'est pas très utile, car nous savons que dans certaines / beaucoup de situations pratiques, cela semble fonctionner assez rapidement - et nous ne savons pas vraiment pourquoi.

Nous ne savons pas pourquoi cela est vrai pour les solveurs SAT, encore moins pour QFBV. Comprendre pourquoi les solveurs QFBV sont souvent rapides semble au moins aussi difficile que de comprendre pourquoi les solveurs SAT sont souvent rapides, ce qui dépasse déjà notre niveau actuel de compréhension. Si vous recherchez plus sur ce site, vous pouvez trouver un résumé des tentatives actuelles pour comprendre ce dernier sujet.