1

I have a large SAT/SMT formula ranging over two (disjoint) sets of variables:

  1. a relatively small set X of Boolean variables (< 1000) and
  2. a much larger set Y of Boolean (and perhaps Integer/Real) variables.

My formula is such that the values of the variables from X determine the values of the variables from Y completely. Consequently, it would be great if Z3 prioritized the variables from X when searching for a model (in fact, it would be even better if Z3 did not branch on any of the variables from the set Y).

Is there a way to provide this information to Z3?

Dan
  • 1,539
  • 12
  • 23
  • 1
    I know for sure that [MathSAT](http://mathsat.fbk.eu/index.html) has a function called `msat_add_preferred_for_branching` in its API which can be used for exactly this situation. I couldn't find its z3 equivalent by navigating the github repository, though.. so I am also interested in the answer to this question. It looks like [something similar has already been asked](https://stackoverflow.com/questions/33885295/z3-is-it-possible-to-adjust-the-branching-heuristics-in-z3) in the past, but perhaps something has changed. – Patrick Trentin Dec 21 '19 at 22:38
  • 1
    I recommend filing an issue at https://github.com/Z3Prover/z3/issues to ask if an API might be available. (Note that this will definitely not be via the smtlib interface, but using the programmatic API somehow.) – alias Dec 22 '19 at 18:11

0 Answers0