CODEWITHSUNDEEP
z3
Ashiq
Ashiq

Reputation: 307

How do I find the memory and time required for modeling/checking the satisfiability in Z3 (NET API)

I am working with Z3 and Yices for less than a year for solving some research problems. Working with these solvers, I always need to evaluate the performance, especially two things: time and space (memory) required for modeling/checking (the satisfiability). In case of Z3, I found no clue to find them directly. I tried with the "statistics" (using the function "DisplayStatistics" provided by Z3 NET API), and found the output as shown (e.g.) below:

num. conflicts: 122

num. decisions: 2245

num. propagations: 27884 (binary: 21129)

num. restarts: 1

num. final checks: 1

num. min. lits: 52

num. added eqs.: 3766

num. mk bool var: 2782

num. del bool var: 658

num. mk enode: 1723

num. del enode: 78

num. mk clause: 3622

num. del clause: 1517

num. mk bin clause: 3067

num. mk lits: 18935

num. ta conflicts: 28

num. add rows: 5091

num. pivots: 328

num. assert lower: 2597

num. assert upper: 3416

num. assert diseq: 1353

num. bound prop: 787

num. fixed eqs: 697

num. offset eqs: 866

num. pseudo nl.: 34

num. eq. adapter: 820

I do not know how to interpret these values to understand the used memory/time. There is some way to find the running time (using timer classes like Stopwatch). But, in case of space requirement, I did not find any way. If I can get the number of Boolean variables (low level, SAT solver) required for modeling could work very well for me.

It would be great, if anyone can show me the solution.

Upvotes: 2

Views: 425

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Which version of Z3 are you using? The latest version (Z3 3.2) includes memory consumption statistics. It will be displayed as max. heap size. That being said, the best way to evaluate Z3's performance is to use z3.exe. The Z3 executable will report time and memory consumption. Moreover, some performance improvements are not yet available through the API.

For several applications the textual interface is the ideal option. That is, your application communicates with the Z3 process using SMT 2.0 commands through a pipe. The main advantages are: it is very easy to use different SMT solvers and compare them; it is easy to kill Z3 and restart it; you can create several different processes; if Z3 dies your application does not die. Of course, this solution is not good for applications that perform thousands of easy queries, or require a tight integration with Z3 (e.g. Scala^Z3).

Upvotes: 2

Related Questions