Back to Index

WalkMINQBF

WalkMINQBF 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:

• First we divide the QBF in two parts: The Existential and the Universal.
• The universal part is sent to the MINSAT module of the algorithm to try to get MINSAT approximations to the universal part of the QBF formula.
• Using the MINSAT approximations, a sub-formula is generated using only the existential part of the formula.
• The sub-formula is sent to the SAT solver (in this case we used KCNFS).
• If an UNSAT is found then the QBF formula is reported as UNSAT.
• If SAT is found the process is repeated until it finds an UNSAT formula or the time ends and UNKNOWN is outputted.

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 sub-formulas from the different assignments that the MINSAT part generates. Basically what is done is to mark the clauses that are important to the sub-formula 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 sub-formula.

Downloads

WalkMINQBF (TAR.GZ)

User's Manual (HTML)

Experiments and Results

Some experiments were run to test the efficiency of the algorithm. The test bed was composed of Random (2,3) QBF Formulas with the following parameters: c=10.0,10.3,10.5,10.7,11.0 and n=80,100,200,300.

WalkMINQBF was tested against SSOLVE and QuBE (Two state of the art QBF Solvers known to be the best random QBF formula solvers) and proved to be better on solving the instances used on these tests.

The test cases used are known to be very difficult to be solved by the regular DPLL algorithms. In fact, SSOLVE and QuBE solved some part of the problems but not as outstanding as the WalkMINQBF solver did.

We now the following facts about our test bed:

• Less ratio than 10.50 means harder formulas
• More variables implies harder formulas
• After 10.50 the formulas became more easy to solve

We tried the ratio 10.50 with different number of variables and we found that WalkMINQBF is better that SSOLVE and QuBE. In fact at ratio 10.50 after 100 existential variables SSOLVE is not capable of solving any formula.

As you can notice from the next chart, SSOLVE and QuBE have a very similar behavior when solving our tests and both are less efficient to show unsatisfiability of the formulas than our algorithm.

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 2-SAT condition of the existential part so we decided to use 5-CNF formulas with 3 existential variables per clause.

Downloads

Benchmarks (TAR.GZ)

Related Tools

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.

Back to Index