How to get the model with minimum variables to satisfy the assertion using Z3

Question

An Example：

from z3 import *
p1,p2, p3 = Reals('p1 p2 p3')
s = Optimize()
s.add(And(Or(p1>=0, p2>0),Or(p1<=10,p3>0)))
print(s.check())
print(s.model())

run the code,and get output:

sat
[p3 = 1, p1 = 11, p2 = 1]

it's right. However, it's valuable to get expected result(satisfy the constraintAnd(Or(p1>=0, p2>0),Or(p1<=10,p3>0)), with setting less variables.

for example, only set p1=0 (or any value in range([0,10])), then the constraint is satisfied. Only one variable is neccessary to set.

so my question is, is there a common method to get the least number of neccessary variables?

Answer 1

What you are looking for are called "symbolic" models, i.e., where some variables are set to constants and others can be set to expressions. For instance, if you have a constraint like x > y, then a symbolic model might be y = 0, x > y. Unfortunately, SMT solvers do not provide "symbolic" models of this sort. The usual DPLL style constraint propagation do not allow for this sort of easy symbolic model construction.

One of the difficulties in this area is the fact that there is no "canonical" notion of what a minimal such model might be. (This question is undecidable in general.)

If you are interested in such models, your best bet is to use higher-level tools like mathematica, or theorem provers in general, to come up with such models. (Of course, these will be semi-automated at best.) BDD based solvers can also provide symbolic models as well, though most modern solvers use SAT engines and/or do not expose enough API to look into models generated by their BDD engines.