0

I am working on a problem with combining multiple objectives lexicographically. First objective is the MaxSMT objective. Is there any way I can extract all the possible assignments after the first MaxSMT optimization?

Thanks

Kshitij Goyal
  • 61
  • 7
  • You need to use the API: fix the optimum MaxSMT value, then enumerate all possible solution as usual. Related Q/A: [1](https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models), [2](https://stackoverflow.com/questions/40459119/how-to-get-multiple-solutions-for-z3-solver-in-smt2-format-example) , [3](https://stackoverflow.com/questions/47873014/z3-finding-all-possible-solutions-using-c-api), [4](https://stackoverflow.com/questions/15256437/z3-number-of-solutions), [5](https://stackoverflow.com/questions/23635348/z3-enumerating-all-satisfying-assignments) – Patrick Trentin Oct 11 '19 at 10:23
  • It is unclear why you don't want to fix the optimum value of the other objectives though. Are you trying to extract the Pareto-front after the first goal has been fixed? – Patrick Trentin Oct 11 '19 at 10:30
  • So I want to look at all possible solutions from the first objective (MaxSMT) to manually calculate the optimum for the second objective. This is just a verification exercise. – Kshitij Goyal Oct 11 '19 at 11:09
  • Unless your other objectives are also of Pseudo-Boolean/MaxSMT type, this might not even be possible. Anyway, leave only the first MaxSMT goal in the formula and enumerate all possible solutions as done in the linked Q/A. -- Note that this is drastically less efficient than letting `z3` find the optimal solution on its own. – Patrick Trentin Oct 11 '19 at 11:14
  • Yeah this helps, thanks! I know this is going to be super inefficient. I just want to understand how the algorithm chooses the final output. – Kshitij Goyal Oct 11 '19 at 11:16
  • @PatrickTrentin Please turn your comment into an answer. It should be accepted. – alias Oct 11 '19 at 13:35
  • @alias This might be an instance of an X/Y problem, see the new question asked by OP. Before posting an answer that solves the question but not the problem at hand, I would wait for further clarifications. – Patrick Trentin Oct 11 '19 at 13:39
  • Sounds like it! – alias Oct 11 '19 at 14:10

0 Answers0