Branch & Bound approach with uninterpreted sorts ?

[pcarbonn]

In so-called generative configuration problems, the number of components in a configuration is not known in advance . For example, a vehicle may have 1, 2, 3 or 4 wheels, a number to be determined subject to some constraints on cost and required functionality.

Such a problem could be represented in Z3 using an uninterpreted sort Wheel for wheels, so that Z3 would generate wheels as needed. Preliminary investigations show that Z3 tends to create more wheels than needed, significantly impacting performance (because the search space increases with the number of created objects).

A Branch & Bound approach could improve performance significanlty: via a setting, we would tell Z3 to create no more than N objects. N would initially be a small number, possibly resulting in unsat. It would then be incremented until sat.

Could that be implemented in Z3 ? I would think it would have other applications as well.

(Related, closed issue: #5672)

[NikolajBjorner]

You can use assumption literals to bound number of wheels. If the assumption literal appears in an unsat core you create a weaker bound using a new assumption literal.
There is an analogy with bounded model checking: search for a short counter-example, then extend the trace size.
There is an example of bounded model checking here http://theory.stanford.edu/~nikolaj/programmingz3.html#sec-bounded-model-checking.
A different avenue may be to describe such problems as MaxSAT, where you are minimizing number of wheels.

[pcarbonn]

Thank you for your reply.

I'm not sure I understand how to create "an assumption literal to bound the number of wheels". I see no mechanism to bound the number of elements in one uninterpreted sort, let alone in all of them (wheels, windows, doors, ...). The bound should be on the total number of components, whatever its sort. Please clarify.

One option I have seen is to have only one interpreted sort of so-called "configuration object" (CO), and use predicates to implement sub-types (wheels, doors, ...). The number of elements in the interpreted sort CO is incremented as needed until sat. That can work indeed, but the theory is more complex to write (because one usually wants to quantify over the sub-types, not over CO) (but that can be managed), and it probably has performance issues, because quantifications are over a larger set (over CO vs over sub-types). In one axiom of a configuration problem, I have 5 nested quantifications over the configuration objects CO: performance degrades very quickly. I would hope that performance can be improved by quantifying over the sub-types instead, with an overall bound on the number of components. (But I may have misconceptions over the internals of Z3.)

[NikolajBjorner]

E.g., introduce constants c1 c2 c3 c4 and assert bound4 => forall x . x = c1 or x = c2 or x = c3 or x = c4, and check-sat assuming bound4?

Quantifiers + assignment problems are perhaps not great. If unfolding quantifiers is possible it can be much more efficient than frugal instantiation.

[pcarbonn]

Got it. Thanks.

[pcarbonn]

Still, I would think that my proposal would have much better performance (if feasible). Wouldn't it ?