Observable-Sharing dramatically increases solver run-time when sharing few expressions

[bruderj15]

The sharing obviously yields big benefits for instances where we actually share a lot. However, for all my instances where there is barely gain from sharing, solver-runtime dramatically increases. My use-cases in general do not offer a lot of sharing, I guess equally for the average user.

Also to note that big instances - with sharing enabled - often lead to the solver crashing (memory - too many vars).

Therefore default SharingMode to None .

[fabeulous]

I observed the same performance decrease where sharing is not used a lot. In applications where sharing leads to significantly smaller formulas, I unsurprisingly do see better results. However, this is likely not the common case and I would agree that disabling sharing by default is the way to go.

I usually know which sub-formulas should be shared for a given encoding. The main benefit I got from the observable sharing approach was simplicity. Especially in combination with the "constant folding", I don't have to worry if my shared subformula could be eliminated since the sharing only happens after formula construction.