Z3 Optimization, strict inqualities

Question

I'm having a problem which was referred to before where I do not quite get the solution (combining substitute with simplify). In my encoding, I have strict inequalities and I would need to set the epsilon either to 0 or to a very small value. For instance, I have the following simplified Python code:

from z3 import *

p = Real('p')
q = Real('q')
s = Optimize()

s.add(p > 0, p < 1)
s.add(q > 0, q < 1)
h = s.maximize(p)

print s.check()
print s.upper(h)
print s.model()

How can I get p to be assigned the maximal value 1? (Right now it is assigned 1/2.) Thanks a lot!

Answer 1

Premise:

1. I assume that you simply want a model in which p approaches 1 with a fixed precision.

2. In this answer N.B. states (emphasis is mine)

epsilon refers to a non-standard number (infinitesimal). You can set it arbitrarily small. Again the model uses only standard numbers, so it picks some number, in this case 9.

Given that..

• I could not find any option to set epsilon neither in the Python API nor among smt2 options

• By changing the size of the interval of x, the value of x in the returned model is at a different distance from the optimal value (e.g. interval 0, 10 gives x=9, whereas 0, 1 givesx=0.5)

..my take of the previous quote is that z3 picks some random satisfiable value, and that's it.

---

Therefore:

I would do it in the following way:

from z3 import *

epsilon = 0.0000001

p = Real('p')
q = Real('q')
s = Optimize()

s.add(p > 0, p < 1)
s.add(q > 0, q < 1)

s.push()
h = s.maximize(p)

print s.check() # Here I assume SAT

opt_value = h.value()

if epsilon in opt_value: # TODO: refine
    s.pop()
    opt_term = instantiate(opt_value, epsilon) # TODO: encode this function

    s.add(p > opt_value)

    s.check()

    print s.model()
else:
    print s.model()
    s.pop()

Where instantiate(str, eps) is a custom-made function that parses strings in the shape of ToReal(1) + ToReal(-1)*epsilon and returns the result of the obvious interpretation of such string.

----

I'd like to mention that an alternative approach is to encode the problem as an smt2 formula and give it as input to OptiMathSAT:

(set-option:produce-models true)

(declare-fun p () Real)
(declare-fun q () Real)

(assert (and (< 0 p) (< p 1)))
(assert (and (< 0 q) (< q 1)))

(maximize p)

(check-sat)
(set-model 0)
(get-model)

OptiMathSAT has a command-line option -optimization.theory.la.epsilon=N to control the value of epsilon within the returned model of the formula. By default N=6 and epsilon is 10^-6. Here is the output:

### MAXIMIZATION STATS ###
# objective:      p (index: 0)
# interval:     [ -INF , +INF ]
#
# Search terminated!
# Exact strict optimum found!
# Optimum: <1
# Search steps: 1 (sat: 1)
#  - binary: 0 (sat: 0)
#  - linear: 1 (sat: 1)
# Restarts: 1 [session: 1]
# Decisions: 3 (0 random) [session: 3 (0 random)]
# Propagations: 6 (0 theory) [session: 13 (0 theory)]
# Watched clauses visited: 1 (0 binary) [session: 2 (1 binary)]
# Conflicts: 3 (3 theory) [session: 3 (3 theory)]
# Error:
#  - absolute: 0
#  - relative: 0
# Total time: 0.000 s
#  - first solution: 0.000 s
#  - optimization: 0.000 s
#  - certification: 0.000 s
# Memory used: 8.977 MB
sat
( (p (/ 1999999 2000000))
  (q (/ 1 2000000)) )