NoneType output from the z3 model

Question

I'm using the MaxSMT to find a solution to a set of soft constraints and hard constraints. With a timeout of 600 secs, the model output I get from the solver is Nonetype for all of the parameters. I was expecting the solver to provide me with a sub-optimal solution. Am I wrong to assume that. Can someone please explain that?

Edit: So I added the verbose option to print out the intermediate steps: I get the following message :

(optimize:check-sat)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 2)
(smt.simplifying-clause-set :num-deleted-clauses 1)
(smt.restarting :propagations 417 :decisions 948 :conflicts 101 :restart 100 :restart-outer 110 :agility 0.000299947)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 3497 :decisions 11262 :conflicts 202 :restart 110 :restart-outer 110 :agility 0.00588127)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 10138 :decisions 18514 :conflicts 313 :restart 100 :restart-outer 121 :agility 0.001524)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 16862 :decisions 21147 :conflicts 426 :restart 110 :restart-outer 121 :agility 0.0337523)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 17827 :decisions 24053 :conflicts 537 :restart 121 :restart-outer 121 :agility 0.0268182)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 25141 :decisions 36272 :conflicts 660 :restart 100 :restart-outer 133 :agility 0.00362989)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 35575 :decisions 47933 :conflicts 765 :restart 110 :restart-outer 133 :agility 0.00289772)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.restarting :propagations 39641 :decisions 52637 :conflicts 876 :restart 121 :restart-outer 133 :agility 0.000965057)
(smt.simplifying-clause-set :num-deleted-clauses 0)
(smt.simplifying-clause-set :num-deleted-clauses 0)
        (smt.restarting :propagations 40803 :decisions 57913 :conflicts 998 :restart 133 :restart-outer 133 :agility 0.0349118)

It seems like the solver is not ale to find a feasible solution. Does it mean that none of the soft constraints are satisfiable?

Does the solver print `SAT`? What is the output of `(get-objectives)` after `(check-sat)`? Could you please share the SMT model? — Patrick Trentin, Nov 13 '19 at 17:12
Did it find any partial solution within the timeout? (use option `-v`). Otherwise, you may have to increase the timeout. — Patrick Trentin, Nov 13 '19 at 17:57
I wouldn't expect `z3` to print any model without even a partial solution. — Patrick Trentin, Nov 13 '19 at 18:02
Let us [continue this discussion in chat](https://chat.stackoverflow.com/rooms/202345/discussion-between-kshitij-goyal-and-patrick-trentin). — Kshitij Goyal, Nov 14 '19 at 14:18
Patrick already explained how to use `-v` here: https://stackoverflow.com/questions/57982965/how-to-check-progress-for-z3-optimization-problem/57987274#57987274 — alias, Nov 14 '19 at 16:30

alias · Answer 1 · 2019-11-14T03:34:26.610

There's no reason to expect to get a "sub-optimal" solution after a time out. Unless the solver comes back with a definite answer, any internal information you can glean is just that: Some internal value that may or not may not be relevant. More importantly, there is no reason to expect that it'd even be a satisfying instance. See this answer for some further details: How to check progress for Z3 optimization problem

If you're in a time-crunch and can't afford to wait, your best bet maybe to iterate yourself: Instead of using the optimizing engine, just do a regular query, evalute your cost function and call the solver again, with the additional constraint that the cost should be smaller than what you got before. While this obviously doesn't necessarily converge to an optimal solution, it gives you the control on how many iterations you want to make, and can work sufficiently well in practice. See the discussion on this question for some further insight: Scalability of z3

NoneType output from the z3 model

1 Answers1