CODEWITHSUNDEEP
z3smt
brokendreams
brokendreams

Reputation: 877

Force Z3 to explore certain candidate space first?

I had a question on smt-solvers (like Z3) and was wondering if you know any Z3-tactic which can help me achieve my objective.

I want to know whether it is possible to force Z3 to explore some variables before exploring other variables.

For examples, I have a scenario where my MaxSMT problem has the following hard constraints 

X1 + X4 >=3
X2 + 7  >=3
X3 + 8  >=3

And the soft-constraint is 

X4 == 0

Here I want to force the smt-solver to first explore candidate space with different values for variable X1. (I believe by default Z3 will randomly explore different values of X1, X2, X3, X4)

So my question is - is there any tactic in Z3 that allows me to tell the Z3-solver what candidate space (set of variables) should it try exploring first?

Upvotes: 0

Views: 188

Answers (2)

Pierre Carbonnelle
Pierre Carbonnelle

Reputation: 2615

One option is to use the cube method of the Solver class. It allows you to specify the variables to use for case split.

Upvotes: 0

alias
alias

Reputation: 30418

The max-smt engine allows user parameterization in z3, but unfortunately it isn't clear if any of these tweaks would allow you to do what you want. But you can at least ask for what the "tweaks" are by using the z3 -p command and looking through the list. I found the following params:

[module] opt, description: optimization parameters
    maxres.add_upper_bound_block (bool) (default: false)
    maxres.hill_climb (bool) (default: true)
    maxres.max_core_size (unsigned int) (default: 3)
    maxres.max_correction_set_size (unsigned int) (default: 3)
    maxres.max_num_cores (unsigned int) (default: 4294967295)
    maxres.maximize_assignment (bool) (default: false)
    maxres.pivot_on_correction_set (bool) (default: true)
    maxres.wmax (bool) (default: false)
    maxsat_engine (symbol) (default: maxres)

(There are others, but these seem most relevant.)

To see how these impact the search, your best bet is probably to read through the source code: https://github.com/Z3Prover/z3/blob/master/src/opt/maxres.cpp

Alternatively, you can try asking at z3 github site (https://github.com/Z3Prover/z3/issues), and the authors might point you in a better direction.

Upvotes: 0

Related Questions