8000 the meaning of unknown in an optimization problem, and intermediate (nonoptimal) solutions. · Issue #1463 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

the meaning of unknown in an optimization problem, and intermediate (nonoptimal) solutions. #1463

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
oferst opened this issue Jan 26, 2018 · 4 comments
Closed

the meaning of unknown in an optimization problem, and intermediate (nonoptimal) solutions. #1463

oferst opened this issue Jan 26, 2018 · 4 comments

Comments

@oferst
Copy link
oferst commented Jan 26, 2018 •
edited
Loading
  1. If I stop Z3 before termination and get
    unknown
    (objectives
    ( (66 1039))
    )
    (model
    ...

does this mean that it found a feasible solution (i.e., satisfies all the hard constraints), but not the optimum ? it makes more sense to me that the status should be 'sat' rather than 'unknown'. Perhaps there should be a new status 'sat but not known if optimal'.

  1. could be great to give it the option to print non-optimal solution during run-time. Having the ctrl^c option is not always good enough when it is a long run-time: you do not know whether the solution is good enough to stop the engine or whether it even found a first solution. So while pressing ctrl^c tells you this, it also stops the process.
    A nice interface to this is e.g., the one in cplex. There you can give it a parameter CPX_PARAM_INTSOLFILEPREFIX with the prefix of the solution files that it will emit during the run.
@NikolajBjorner
Copy link
Contributor

Makes sense.

NikolajBjorner added a commit that referenced this issue Jan 28, 2018
@NikolajBjorner
add solution_prefix per #1463, have parto with single objective behav…
e4198c3 
…e similar to multipe-objectives #1439

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@oferst
Copy link
Author
oferst commented Jan 30, 2018

Thanks for implementing this! Two comments:

  1. It is better (i.e., consistent with other tools) if it will also emit the optimal (final) solution as a file with that prefix. So I fixed it by adding
    model_ref mdl;
    s().get_model(mdl);
    m_c.model_updated(mdl.get());

in opt/maxres.cpp line 327, in case you want to add it too.
2. Ideally this feature should be global so it works with other supported formats, e.g., opb and wcnf (by the way currently in those formats ctrl-c does not produce the current solution).

@oferst
Copy link
Author
oferst commented Jan 30, 2018

My apology for item #2 in the previous post: the solution_prefix is already supported globally.

@NikolajBjorner
Copy link
Contributor

Ah, I thought you wanted the output format to follow opb/wcnf format rules when the input is in this format. That is a valid ask, but something I would not like to do. The other optimization modules don't call into the model_updated functionality yet, but I take you only use maxsat at this point.

NikolajBjorner added a commit that referenced this issue Jan 30, 2018
@NikolajBjorner
adding initial model to updated #1463
73e9d35 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
5A3C @NikolajBjorner NikolajBjorner closed this as completed in e1100af Feb 12, 2018
@bruderj15 bruderj15 mentioned this issue Sep 26, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@NikolajBjorner @oferst
0