Hinting to Z3

[JasonKleban]

I believe this has been discussed a bunch of times, but I haven't seen an answer that I can recognize and apply to my understanding of Z3.

Let's say we have thirty highly constrained Ints domain with solution values somewhere 0..99 each. The changes along each domain are non-linear and have a specific but unmathematical(?) pattern.

I have an implementation of this, and I can get sensible answers within a minute when I tell it to honor the constraints on only, say. 10 of the domain constants. Letting it loose on more than that seems to grow the problem like crazy such that I can run it at full speed for 24 hours with no result.

My human mind is too feeble to find the solution alone, but my Z3-based implementation is possibly reduced still to brute force guessing and testing, I imagine.

If my human mind suspects that each domain has an answer that is close to 24 or 67 or whatever for each one, is there a way to weight something for Z3 so that it begins its search from those epicenters instead of starting at 0, as I imagine it might be doing?

[NikolajBjorner]

Yes, it is likely lemma learning produces nothing of value.

Could you try local search options?
https://microsoft.github.io/z3guide/programming/Local%20Search

[JasonKleban]

Thanks! Can you please explain more than that link does about what Local Search to improve the chances of solving my kind of problem? I see it's some options to enable, but without actually giving it some new insights this seems like a magic wand?

[NikolajBjorner]

It starts with a candidate solution to variables and updates one variable at a time in order to find a global satisfying assignment. It uses lookahead to select a most promising update. Local search solvers can sometimes find solutions where complete solvers (with lemma learning) struggle. You can use it stand-alone as a tactic or as an option when using the main solver (in parallel or periodic).
Z3 doesn't contain brute force CP with forward pruning, which could also be a candidate for the style of problems you describe.

[JasonKleban]

Followup question - Especially with local search, is there a way to periodically sample from Z3 the bindings to my constants that its most recently tested and perhaps the number of assertions that pass/fail?

I believe that a non-local-search wouldn't be very useful to look at as it iterates through ordered or random guesses, BUT it could be timed-out and restarted as often as I wanted an illustration (assuming I could extract those unsat guesses).

My app-level illustration would be 30-wide column chart or candlestick and another illustration of satisfaction of individual assertions (which I don't know how to reference using the z3 api, btw)

A local search's guesses would be more interesting to watch but I don't see how it could be interrupted and resumed using timeouts. Is there another way to poll for this?

[JasonKleban]

Adapting that "Local Search" documentation parameters to the Z3 .net api (F#) this is the closest I'm finding, setting these parameters on the solver itself:

    let s = ctx.MkSolver()

    s.Set("arith.random_initial_value", true) // seems better than starting at 0
    s.Set("local_search", true)

(No warnings for those choices now, but takes about the same time to solve my reduced constraints set.)