Incomplete MaxSAT

[kgoyal40]

I have a problem where I am considering to use incomplete MaxSAT algorithms. Are there any incomplete MaxSMT solvers implemented in z3?

[NikolajBjorner]

You can register a callback with the Optimize object that returns intermediary solutions.
So far I support the callback for the python API. You can also enable the parameter "opt.enable_lns", which when used from the default maxsat solver uses some improved search for intermediary solutions. While it remains to be further tuned, it can offer much higher quality solutions than the default option on hard MaxSAT problems.

The option is called enable_lns=true, example:

opt = Optimize()
opt.set(“enable_lns”, True)

From the command-line use “opt.enable_lns=true”.

You can also get intermediary solutions from a callback in Python

def on_model(model):
       print(model)

opt.set_on_model(on_model)

Then:

opt.from_file(my_file)
opt.check()

[kgoyal40]

Thanks for the reply. I've updated the z3 solver, but the latest version still seems to be 4.8.10 which doesn't have the “enable_lns” option. When will the 4.8.11 version be published?

[NikolajBjorner]

You can download bits from "nightly" releases.

[kgoyal40]

@NikolajBjorner Can you tell me which bits i should download from the nightly releases?

[NikolajBjorner]

https:/Z3Prover/z3/releases/tag/Nightly
For your platform:
z3-4.8.11-x64-glibc-2.31.zip (Linux)
z3-4.8.11-x64-osx-10.15.7.zip
z3-4.8.11-x64-win.zip
z3-4.8.11-x86-win.zip