Arithmetic conflicts vs conflicts in Z3 solver statistics

1
votes

I am studying two QF_LIA satisfiability based task scheduling problems using Z3.

Questions

  1. What is the difference between arith-conflicts and conflicts in the statistics reported by Z3?

  2. Is one of these metrics a good way of quantifying how easy/hard it was for Z3 to solve the problem? I find that solve time for the first case is lower than the second, I am trying to support this/explain this using some solver statistics measured by Z3.

  3. Problem 1 has more clauses than problem 2 (61k vs 10k). But I see a huge difference in arith-add-rows (1M vs 7M). What does this field mean?

Statistics for Problem 1

Solve time: 5s

Z3 Stats:

(:arith-add-rows 1274977 :arith-assert-lower 631097 :arith-assert-upper 1736529 :arith-bound-prop 84528 :arith-conflicts 938 :arith-pivots 11305 :binary-propagations 2934957 :conflicts 10288 :decisions 30244 :del-clause 14335 :eliminated-vars 54 :final-checks 1 :max-memory 26.31 :memory 11.47 :minimized-lits 52633 :mk-bool-var 9577 :mk-clause 61136 :num-allocs 62610792 :propagations 5336053 :restarts 9 :rlimit-count 60060905)

Statistics for Problem 2

Solve time: 12s

Z3 Stats:

(:arith-add-rows 7360423 :arith-assert-lower 98284 :arith-assert-upper 106749 :arith-bound-prop 7940 :arith-conflicts 3859 :arith-pivots 24323 :binary-propagations 77194 :conflicts 4190 :decisions 13619 :del-clause 1012 :eliminated-vars 64 :max-memory 21.89 :memory 4.69 :minimized-lits 14385 :mk-bool-var 3329 :mk-clause 10681 :num-allocs 33767877 :propagations 236651 :restarts 7 :rlimit-count 608859507)

1
z3

1 Answers

2
votes

  1. My understanding is that conflicts counts the number of literal assignments that Z3 tried but that later on turned out to yield a conflict. My guess thus is that arith-conflicts counts the number of conflicts the arithmetic subsolver(s) caused.

  2. A high number of conflicts could indicate that Z3 didn't proceed very goal-directed, i.e. that it explored parts of the solution candidate space without actually finding a solution. That's my interpretation of conflicts, though; not sure of the Z3 team would agree.

  3. No idea what arith-add-rows means. You could grep Z3's sources to see where it is incremented.