Eu tento usar o resolvedor z3 para um problema de minimização. Eu estava tentando obter um tempo limite e retornar a melhor solução até agora. Eu uso a API python e a opção de tempo limite "smt.timeout" com

set_option("smt.timeout", 1000) # 1s timeout

Na verdade, isso expira após cerca de 1 segundo. No entanto, um tempo limite maior não fornece um objetivo menor. Acabei ligando a verbosidade com

set_option("verbose", 2)

E acho que o z3 avalia sucessivamente valores maiores do meu objetivo, até que o problema seja satisfatório:

(opt.maxres [0:6117664])
(opt.maxres [175560:6117664])
(opt.maxres [236460:6117664])
(opt.maxres [297360:6117664])
...
(opt.maxres [940415:6117664])
(opt.maxres [945805:6117664])
...

Portanto, tenho as duas perguntas:

Por outro lado, posso dizer ao z3 para começar com o limite superior e retornar modelos sucessivamente com um valor menor para a minha função objetivo (como, por exemplo, as anotações do Minizincindomain_max http://www.minizinc.org/2.0/doc-lib/doc-annotations-search.html)Ainda parece que o solucionador retorna uma instância satisfatória do meu problema. Como é encontrado? Se estiver tentando avaliar valores maiores do meu objetivo sucessivamente, ainda não deveria ter encontrado uma instância satisfatória quando o tempo limite ocorrer ...

editar: No log opt.maxres, o limite superior nunca diminui.

Para o registro, encontrei uma descrição mais detalhada das opções na fonte aquiopt_params.pyg

Editar Desculpe incomodar, estive mergulhando nisso recentemente mais uma vez. De qualquer forma, acho que isso pode ser útil para os outros. Descobri que na verdade tenho que ligar para oOptimize.upper para obter o limite superior e o modelo ainda não é o que corresponde a esse limite superior. Consegui adicioná-lo como uma nova restrição e chamar um solucionador (sem otimização, apenas SAT), mas essa provavelmente não é a melhor idéia. Pela leituraesta Eu sinto que deveria ligarOptimize.update_upper após o tempo limite do solucionador, mas a interface python não possui esse método (?). Pelo menos eu posso obter o limite superior e o modelo correspondente agora (ao custo de cálculos desnecessários, eu acho).