sambayless
commented
4 years ago 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
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?