Huge performance improvement when using the QF_FD logic

[sirwhinesalot]

I know it might sound strange to complain about a huge performance improvement, but I was just wondering if this is intended.
I'm solving the boolean n-queens problem in a variety of solvers to test their ALL-SAT performance. I use blocking clauses to implement ALL-SAT search in Z3.

As expected, CP solvers (specially ones based on MAC) absolutely dominate the challenge with their built-in DFS search.
Z3 was giving me a rather disappointing 11 seconds for a 10x10 board, even after explicitly using pseudo-boolean constraints.

But then I switched to the "QF_FD" logic explicitly (before I just let the solver pick), and now it takes 200ms, not quite Gecode but two orders of magnitude better is huge. Not only that, I get the excellent performance even if I don't use pseudo-boolean constraints explicitly, Z3 seems to detect it's a pseudo-boolean problem automatically somehow?

My question is, shouldn't the solver be able to detect that the problem is in the QF_FD logic automatically if every variable is a Boolean? It would be nice to not have to explicitly request it.

Note: I tried with QF_BV just out of curiosity and it gave incorrect results (1 extra solution) consistently for different board sizes. I was actually surprised it worked at all, I wasn't expecting z3::sum to work on Boolean variables without converting them to integers or bit vectors first using z3::ite(b, 1, 0) for example, at least not without QF_FD explicitly set.

EDIT: actually, on higher board sizes, using the PB constraints explicitly actually gives worse results somehow...

[NikolajBjorner]

QF_FD uses transformations that convert arithmetic to Booleans/Bit-vectors/Cardinality constraints. It then uses a more efficient solver core.
QF_FD requires that the formulas be in a small finite domain fragment. It can be unsound or incomplete.

Z3's front-end allows arithmetic on Booleans. It is too tedious to always wrap them in an if-then-else when z3 can do it internally.
This is similar to MIP solvers that allow you to declare 0-1 variables (Booleans) and perform arithmetic on them.
The internal representation is still if-then-else expression, but the QF_FD pre-processing detects cases where arithmetic can be eliminated in favor of Pseudo-Boolean constraints.

Not sure about QF_BV the unsoundness.

[sirwhinesalot]

I see, so the issue is that QF_FD can be unsound/incomplete and so Z3 doesn't "risk it" so to say. Though with every variable being a boolean this should be a safe optimisation IMO.

From what I understand when using incremental solving (like in my ALL-SAT case), Z3 also falls back to the general SMT engine if a specific solver type is not requested. Here it may also make sense to stay in the automatically selected backend for the first solve (if it is incremental) as long the new added constraints remain in that fragment.

Just thinking out loud here, as the performance difference is astounding. Either way, I'm very pleased with the performance of the QF_FD solver for my use cases, and I very much enjoy the fact that Z3 automatically translates booleans to if-then-else when needed, as that is indeed annoying.