Interpretation of Z3 Statistics

问题:

I obtained several statistics from runs of Z3. I need to understand what these mean. I am rather rusty and non up to date for the recent developments of sat and SMT solving, for this reason I tried to find explanations myself and I might be dead wrong. So my questions are mainly:

1) What do the measures' names mean?

2) If wrong, can you give me pointers to understand better to what they refer to?

Other observations are made below and conceptually belong to the two questions above. Thanks in advance!

My interpretation follows.

• DPLL. All the metrics below refer to the jargon of the DPLL algorithm which is the foundation of most solvers.

  • :decisions
    • Number of decisions
  • :propagations
    • Number of propagations (I guess unit propagations)
  • :binary-propagations, :ternary-propagations
    • Propagations of two and three literals at once
  • :conflicts
    • Number of conflicts

• RESOLUTION. Operations made interpreting clauses as sets, roughly speaking; techniques taken from resolution which is another paradigm for solving SAT.

  • :subsumed
  • :subsumption-resolution
    • What is the difference between the above two?
  • :dyn-subsumption-resolution
    • Should be described here: Learning for Dynamic Subsumption, by Hamadi et al.

• OTHER TECHNIQUES

  • :minimized-lits
    • No clear idea. Is it probably related with clause learning?
  • :probing-assigned
    • I guess it counts the number of assignment made when "probing", which I guess is some kind of lookahead technique.
  • :del-clause
    • Number of deleted clauses (for what reason? Redundant?)
  • :elim-literals :elim-clauses :elim-bool-vars :elim-blocked-clauses
    • Number of entities after the elim- eliminated. These metrics refer to particular SAT solving techniques (see for reference Blocked Clause Elimination, by M.Järvisalo et al.)
  • :restarts
    • Number of restarts.

• OTHER ASPECTS

  • :mk-bool-var :mk-binary-clause :mk-ternary-clause :mk-clause
    • Number of boolean variables and binary,ternary and generic clauses created.
  • :memory
    • Maximum amount of memory used.
  • :gc-clause
    • Garbage-collected clauses ...?
    • This interpretation is plausible according to my experiments since it's always the case that
      • :gc-clause <= :del-clause ; in my case the disequality is strict.
    • It is not always the case that
      • :gc-clause<=:elim-clauses; it can also be :gc-clause > :elim-clauses

回答1:

I am afraid this is an open-ended question. Z3 exposes many counters that are collected in many different ways. While many capture abstract concepts, their meanings are ultimately based on implementation behaviors of the code.

Fortunately the source code is available and provides the full context for understanding the behavior of each counter. So there is no single document that tracks the meaning of the counters, but the source code is made available to give the full context.