I was initially skeptical about defining Foldable for the direct-style LogicT transformer, but now I suspect that it is definable.
Now that I think about it, you're losing the ability to work with monad transformers.
I think you're right. The particular point of msplit is that it is a monad transformer method and provides certain guarantees on the order and occurrences of _effects_. It seems the interface of Foldable, at brief glance, makes no assurances as to how foldr may behave. The implementation of foldr may decide to `look ahead' of the foldable data structure for optimization purposes and only then start invoking the folding function. That is sound so long as `looking ahead' does not entail any effect. The function `msplit' is designed to operate on a `data structure' where examining each element may be accompanied by an effect. It becomes important then not to look ahead and be careful not to re-do an effect if we need to re-examine some previously seen value. In short, msplit in LogicT does provide guarantees about the effect. The Foldable interface leaves this issue unspecified, or so it seems. So, they can't be considered equivalent. And speaking of non-determinism in general, it seem from experience FBackTrackT is a quite a better solver: it finds solutions where List and similar monads fail to find them; compared to the breadth-first search (which is too, complete), FBackTrackT takes far less resources. So, here too FBackTrackT finds solutions where breadth-first search just runs out of memory.