WalkMINQBFWalkMINQBF is a QBF solver capable of proving unsatisfiability of two alternations QBF. As you can see from previous sections, the solver uses two components: MINSAT Solver that uses a stochastic local search method to find an assignment to the universal variables and a complete SAT solver that will search and test the sub formulas generated by the MINSAT assignment to try to find a UNSAT result.
The figure shows the interaction between the modules of the WalkMINQBF algorithm. The steps it uses to generate a solution is divided in the following steps:
Data structures
In the next picture we can see the main data structures that hold the information of the WalkMINQBF algorithm.
As it was explained before, the algorithm builds several subformulas from the different assignments that the MINSAT part generates. Basically what is done is to mark the clauses that are important to the subformula so it can take into consideration only those when outputting them to the SAT solver.
The formula structure keeps track of all the clauses but it separates them in two groups to make the interaction between the modules more easy. The clauseU array inside the formula keeps track of the Universal part of all the formula while the clauseE keeps the information of the Existential part.
When the solver is initialized the algorithm works similarly to walkSAT. It will fill the arrays of occurrence and clauses while it reads the formula from a file. It uses some of the same structures from walkSAT to obtain the advantage of fast access to the variables and the contents of the clauses.
WalkMINSAT was modified to work directly with the WalkMINQBF structures. In fact, this integration was very straightforward since they share the same basic ideas on the data structures.
When outputting the existential part to KCNFS the SubFormula structure is used and as it was explain before the data is copied so KCNFS can try to prove the unsatisfiability of the subformula.



In addition, to the tests made with the Hubbie’s model of QBF we made some additional experiments with Gent’s Model A and Model B. Those models are used on the QBF competition to test the state of the art QBF solvers. We generated two test groups for the three solvers.
The first test group were formulas based on Model A with 150 variables and ratio = 6 and 8, those formulas are particularly hard for DPLL solvers like QuBEBJ and SSOLVE but not so hard to solve by our algorithm. As we can see in the following picture WalkMINQBF outperforms the state of art algorithms in time and number of formulas proven to be UNSAT. This group of formulas belongs to a family of tests used during the 2004 QBF evaluation; in fact, during the tests also some easier formulas were run on WalkMINQBF with excellent results meaning that the algorithm can help to really improve many of the actual solvers.
The second group was based on Model B and it has similar results to Model A and Hubbie’s model. The group of formulas were constructed using 100 variables and ratios = 10 and 10.50. WalkMINQBF again outperformed the state of art solvers on these formulas that are very hard to solve. In this case we did not use a family of the 2004 QBF evaluation because they were all easily solved by the three solvers, we think it was because of the 2SAT condition of the existential part so we decided to use 5CNF formulas with 3 existential variables per clause.
Benchmarks (TAR.GZ)
As part of the work done to accomplish the task of building WalkMINQBF some tools were built. Some of them can be very useful in the study of QBF. In particular the QBF generator can be very useful and flexible to create almost any kind of Random QBF formula using the Hubbie’s and Interian’s model.
QBF Generator (ZIP) 
This Generator of Random Formulas is based on the generator previously released by Yannet Interian based on the paper of Hubbie Chen and Yannet Interian, but it instead of been restricted to be used to create 2 alternations and 3 alternations QBF formulas it creates any kind of random formulas using the model created by Chen and Interian. 
SubFormula Printer (ZIP) 
This tool will extract the existential part of a 2 alternations QBF formula given an assignment of all the universal variables as input. 
Solution Verifier (ZIP) 
This tool returns the number of SAT clauses of a SAT formula after inputting a solution. It was used as a way to verify that the MINSAT solutions were ok while running the complete algorithm. 