Quaffle
The idea of WalkMinQBF is a great way of solving and proving Random UNSAT formulas. The solver was developed without taking into consideration the ideas of a complete QBF solver as SSOLVE or QuBE-BJ. By itself it will never prove SAT instances nor will prove unsatisfiability of some formulas also it was developed to only solve 2 alternation QBF formulas and we want it to solve any kind of QBF problems. This is why we want to append the ideas of WalkMINQBF to a state of the art QBF solver. After analyzing the sources codes available on the Internet we decided to study Quaffle because it is a well constructed state of the art solver and it can be easily modified to test out ideas on it.
Quaffle is a solver written on C++ by Princeton University. It is written using the object-oriented methodology, and after studying the code we go some general ideas of how to integrate the WalkMINQBF algorithm on it. The main idea is to integrate it as a way of cutting some parts of the search tree without having to go down the tree looking for UNSAT clauses. If it is correctly implemented, it can save a lot of time when looking for UNSAT instances and also can help to find some SAT instances as well. If It prunes the tree it will help making the algorithm go faster.
The first step was to understand the code. I created a little manual that resembles a Java API where I explain each method and field of the code so I can get a reference of where and what to modify in order to insert the ideas of WalkMINQBF into Quaffle. This manual can be found here. It is important to mention that it only gives a general idea of the solver and it is based on my understanding of the code. It can have some missing parts.
After getting a good understanding of Quaffle we know that a first approach can be to insert the WalkMINQBF program into one of the methods of Quaffle without making many changes. It as well as a good implementation of the whole idea is work that can be done in the future and is not part of the present Research Internship Final Report.