Quelles statistiques indiquent une exécution efficace de Z3?

La directive SMTLib2 (get-info all-statistics) affiche plusieurs numéros, par ex.Quelles statistiques indiquent une exécution efficace de Z3?

num. conflicts:  4 
num. propagations: 0 (binary: 0) 
num. qa. inst:  23

Afin de tester différents axiomatisations et codages je voudrais savoir quels de ces numéros sont appropriés pour déclarer qu'un run Z3 est mieux/plus efficace qu'un autre.

Deviner à partir des noms Je dirais que num. qa. inst - le nombre d'instanciations de quantificateurs - est un bon indicateur (inférieur = meilleur), mais qu'en est-il des autres?

Source

2011-07-27 Malte Schwerhoff

Le nombre d'instanciations de quantificateurs est une bonne mesure pour vérifier si votre axiomatisation produit trop d'instances ou non. Vous pouvez également utiliser QI_PROFILE = true. Il produira des statistiques pour chaque quantificateur. Vous pouvez utiliser l'attribut: qid pour donner un nom à un quantificateur. Vous pouvez également utiliser DEFAULT_QID = true et Z3 produira un nom basé sur les numéros de ligne. QI_PROFILE_FREQ = affichera les statistiques après la génération de toutes les instances. Ces options sont utiles pour détecter les boucles d'instanciation. "Nb conflits" est utile pour estimer la taille de l'espace de recherche traversé par Z3. On peut dire qu'une axiomatisation est "meilleure" si la taille de l'espace de recherche est plus petite.

Cheers, Leo

Source

2011-07-27 15:57:14

Merci de remarquer les options supplémentaires! Mais qu'en est-il des autres numéros, par ex. "nombre de décisions"? Lequel d'entre eux devrait être considéré lors de l'analyse comparative des codages Z3? –

"nombre de conflits" est beaucoup plus pertinent que "nombre de décisions". BTW, Z3 utilise backtracking non chronologique. Ainsi, n décisions n'implique pas que Z3 a exploré 2^n branches. "nombre de conflits" est à peu près égal au nombre de branches explorées par Z3. Il existe d'autres nombres utiles pour détecter les goulots d'étranglement dans le raisonnement théorique. Par exemple, "pivots" -> Z3 a des problèmes avec l'arithmétique linéaire, "coupes de gomory" -> arithmétique entière, "interface eqs" -> combinaison de théorie, etc. –

Quelles statistiques indiquent une exécution efficace de Z3?

Répondre

Questions connexes