Add a new proof search strategy through assumptions

[vedadux]

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