0

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?

Community
  • 1
  • 1
Mark Jin
  • 2,616
  • 3
  • 25
  • 37

1 Answers1

1

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.

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30