Which statistics indicate an efficient run of Z3?

问题:

The SMTLib2 directive (get-info all-statistics) displays several numbers, e.g.

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

In order to test different axiomatisations and encodings I'd like to know which of those numbers are appropriate to declare that one Z3 run is better/more efficient than another.

Guessing from the names I'd say that num. qa. inst - the number of quantifier instantiations - is a good indicator (lower = better), but what about the others?

回答1:

Number of quantifier instantiations is a good measure for checking whether your axiomatisation is producing too many instances or not. You can also use QI_PROFILE=true. It will produce statistics for each quantifier. You can use the attribute :qid to give a name to a quantifier. You may also use DEFAULT_QID=true, and Z3 will produce a name based on line numbers. QI_PROFILE_FREQ= will display the statistics after every instances are generated. These options are useful for detecting instantiations loops.

"num. conflicts" is useful for estimating the size of the search space traversed by Z3. We may say an axiomatisation is "better" if the size of the search space is smaller.

Cheers, Leo