CODEWITHSUNDEEP
logicconstraintsz3smtz3py
Mark Jin
Mark Jin

Reputation: 2913

z3: Is it possible to adjust the branching heuristics in Z3?

This is a follow-up question of What is the importance of the order of the assertions in Z3?

Given that Z3 uses DPLL algorithms. Suppose I have some knowledge about which variables are more critical. Is it possible that I make Z3 solver to branch on these variables first when evaluating my logic problem so as to boost the performance or efficiency?

Upvotes: 0

Views: 249

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8392

This is possible but there is no convenient interface for it at the moment. You'd have to hack the source code a bit, but if you really know that you have to branch on particular variables first it may be worth the effort.

Upvotes: 1

Related Questions