vedadux/nanoqbf

A minimal implementation of an expansion-based QBF solver which does not use recursion.

nanoqbf's Issues

Add useful optimisations from Ijtihad

The following features have proven to be useful and should be implemented before the first release:

1. Formula trimming for A and B
2. Reuse of Tseitin variables
3. Depth based clause deduplication (maybe)

Documentation

This needs to be done before I forget what half of the implementation does.

Refactor Formula::getGlobalPosition

This function is horrible for the locality of the data and causes the most cache misses, as it is used in the tight variable replacement loops. A much better way of doing this is first renaming the variables so that their local and global position can be decided directly by the name/index. Something similar was done in Ijtihad.

Add a new proof search strategy through assumptions

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