[z3py] Disable MBQI for z3.Optimize?

[caterinaurban]

It seems that MBQI is enabled by default when creating a solver using the Optimize API, and it does not seem possible to disable it. Using the Solver API the option can be set with s.set(mbqi=True) (for instance), but this raises an exception when using the Optimize API. Is there a reason for this? Is there another way to disable MBQI when using the Optimize API?

[wintersteiger]

A frequent problem with that is that auto-configuration re-enables MBQI. Could you try adding auto_config=false?

[caterinaurban]

The problem is that the Optimize API only allows to set the following options (this is the output of the help() function):

dump_benchmarks (bool) dump benchmarks for profiling (default: false)
elim_01 (bool) eliminate 01 variables (default: true)
enable_sat (bool) enable the new SAT core for propositional constraints (default: true)
enable_sls (bool) enable SLS tuning during weighted maxsast (default: false)
maxres.add_upper_bound_block (bool) restict upper bound with constraint (default: false)
maxres.hill_climb (bool) give preference for large weight cores (default: true)
maxres.max_core_size (unsigned int) break batch of generated cores if size reaches this number (default: 3)
maxres.max_correction_set_size (unsigned int) allow generating correction set constraints up to maximal size (default: 3)
maxres.max_num_cores (unsigned int) maximal number of cores per round (default: 4294967295)
maxres.maximize_assignment (bool) find an MSS/MCS to improve current assignment (default: false)
maxres.pivot_on_correction_set (bool) reduce soft constraints if the current correction set is smaller than current core (default: true)
maxres.wmax (bool) use weighted theory solver to constrain upper bounds (default: false)
maxsat_engine (symbol) select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres' (default: maxres)
optsmt_engine (symbol) select optimization engine: 'basic', 'farkas', 'symba' (default: basic)
pb.compile_equality (bool) compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites) (default: false)
pp.neat (bool) use neat (as opposed to less readable, but faster) pretty printer when displaying context (default: true)
print_model (bool) display model for satisfiable constraints (default: false)
priority (symbol) select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box' (default: lex)
rlimit (unsigned int) resource limit (0 means no limit) (default: 0)
timeout (unsigned int) timeout (in milliseconds) (UINT_MAX and 0 mean no timeout) (default: 4294967295)

So we cannot disable auto-configuration either.

[wintersteiger]

auto-config is a global option, I think in Python z3.set_param("auto-config", "false") should do the trick (before creating the solver to be on the safe side).

[caterinaurban]

This works! Thanks a lot!!

[wintersteiger]

Great, thanks for reporting back!