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
Zhongjun 'Mark' Jin
  • 2,336
  • 3
  • 23
  • 33

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,084
  • 1
  • 14
  • 28