Integration with Z3?

[jeremysalwen]

The interface and design of monosat seems similar to Z3. Is there any chance that you would support using monosat as a theory within Z3, to allow solving problems that have a mixture of graph constraints and other constraints that are better handled by Z3?

[sambayless]

Yes, that should be possible.
monosat is closely based on minisat, and it should be relatively easy to integrate the monotonic theory solvers in monosat into any similar SMT solver (Z3, CVC4).

One challenge for Z3 in particular: I'm not sure if this is true any more, but at once point in the past (6+ years ago) my understanding was that Z3 required theory solver implementations to eagerly construct 'reason' clauses for theory propagated literals, as soon as theory propagation occurs. This is a challenge for monosat's graph theory, for which constructing a 'reason' clause is relatively expensive. For that reason, monosat only constructs reason clauses for theory propagation lazily, at the time they are actually involved in a conflict (which only a small percentage of theory propagated literals typically are).

Its possible that someone with a better understanding of Z3 might be able to shed some light here on the best way to deal with this (or maybe my memory of how Z3 handles theory propagation is wrong).

[jeremysalwen]

Cool, There is also this stackoverflow question which discusses the move from an external plugin API to only supporting an internal plugin API: https://stackoverflow.com/questions/46508907/smt-solver-with-custom-theories

I also asked about supporting monosat theories on the z3 github: #28 and Nikolaj suggested that this could be implemented as a user propagator, which is a newer API but I think is more restricted.