NanoQBF needs more memory than other competitive expansion based QBF solvers. This is in part due to the non-deterministic nature of the expansions it does. This problem is somewhat alleviated using pruning strategies, but those are not enough, as the solver still needs a full expansion for something like the ADDER benchmarks.
The following is an idea of how an improved expansion strategy might look like:
Given is a QBF of the form: \forall x1 x2 \exists y1 y2 \forall x3 x4 x5 \exists y3 y4 y5. \Phi
First say (x1,x2,x3,x4,x5) = (a0,b0,c0,d0,e0) is chosen for the expansion, and we get \Phi_\foral := \Phi[a0,b0,c0,d0,e0]
We find a solution ((y1,y2)^{a0,b0}, (y3,y4,y5)^{a0,b0,c0,d0,e0}) = (f0,g0,h0,i0,j0) and expand to get - \Phi_\exists := -\Phi[f0,g0,h0,i0,j0]
Now, we can try finding a solution and will not see (x1,x2,(x3,x4,x5)^{f0,g0}) = (a0,b0,c0,d0,e0) again
However we might want to restrict ourselves to solutions starting with (x1,x2) = (a0,b0)
Two things can happen on such an assumption:
It succeeds and we find (x1,x2,(x3,x4,x5)^{f0,g0}) = (a0,b0,c1,d1,e1) as a solution
It fails and we learn the clause (x1,x2) \neq (a0,b0) in the negated existential expansion, which is the same as learning the cube (x1,x2) = (a0,b0) in the original QBF
This insight can also be used in the other direction, which will yield clauses in the universal expansion which are also clauses in the original QBF
NanoQBF needs more memory than other competitive expansion based QBF solvers. This is in part due to the non-deterministic nature of the expansions it does. This problem is somewhat alleviated using pruning strategies, but those are not enough, as the solver still needs a full expansion for something like the ADDER benchmarks.
The following is an idea of how an improved expansion strategy might look like: