Conclusions

The SAT and QBF worlds are very interesting and challenging. Improving and generating algorithms to solve both can be translated into solutions of many real-world problems and can help in the development of many techniques that can be applied to other fields of study.

The algorithm developed during this internship has showed to be very good and it could be applied to solve more general QBF instances faster. The algorithm has shown when applied to UNSAT instances that it can give very good and fast results without having to search in the entire space.

WalkMINQBF has outperformed two of the best state of the art QBF solvers demonstrating that this field of study has a lot of work to do in order to improve its techniques. From the given tests beds WalkMINQBF solved more formulas in less time than QuBE-BJ and SSOLVE showing that the idea is very good and have to be used to improve the existent algorithms. Now it will be important to extend this work to a complete solver so we can study its behavior on a complete search and try to adjust the ideas to make the QBF solvers faster.

In order to implement an extension of this algorithm into a complete QBF solver, a heuristic to know when to apply the WalkMINQBF algorithm will be necessary to not spend time trying to find UNSAT instances where it is impossible to find one. The algorithm by itself could be used as a way to prune the search tree but it has to be used carefully to really give an advantage to the search of UNSAT instances.

Finally, while it has been very challenging to learn from scratch about topics like QBF and SAT it has also been very interesting to understand the concepts behind both and to learn about the techniques and heuristics that can be used to solve many computational problems. I hope this work can be applied to the improvement of QBF algorithms to develop new and more sophisticated algorithms capable of solving all kind of QBF problems in both the Random and Practical domains.

References

1. Zbigniew Michalewicz and David B. Fogel. “How to solve it: Modern Heuristics” Second Edition. Springer, Germany 2004.
2. Stuart Rusell and Peter Norvig “Artificial Intelligence A Modern Approach” Second Edition. Prentice Hall. USA 2003.
3. Yannet Interian, Gabriel Corvera and Bart Selman “Finding small unsatisfiable cores to prove unsatisfiability of QBFs” Ninth International Symposium on Artificial Intelligence and Mathematics, 2005.
4. Hubie Chen and Yannet Interian “A model for generating Random Quantified Formulas” in Proc. Of 9^th International Joint Conference on Artificial Intelligence (IJCAI05), 2005.
5. Gilles Denquen and Oliver Dubois. “kcnfs: An efficient solver for random k-sat formulae”. Theory and Applications of Satisfiability Testing: 6^th International Conference, SAT 2003, LCNS, 2003.
6. Bart Selman, Henry Kautz and Bram Cohen. “Local search strategies for satisfiability testing”. Proceedings of the Second DIMACS Challenge on Cliques, Coloring and Satisfiability, 1993.
7. L. Simon, D. Le Berre, M. Narizzan and A. Tachella. “The second QBF solvers comparative evaluation”. 7^th International Conference on Theory and Applications of Satisfiability Testing, 2004.
8. Ian P. Gent and Toby Wash “Beyond NP: the QSAT phase transition”, AAAI 1999, 1999.
9. Brian Borchers and Judith Furman “A two-phase exact algorithm for MAXSAT and Weighted MAXSAT problems” Journal of Combinatorial Optimization, 1999.
10. David Pinto “Determinación de Eficiencia y Factor de Garantía  de un Algoritmo Basado en Búsqueda Local para el Tratamiento del Problema MAXSAT” Thesis for MS Degree Benemérita Universidad Autónoma de Puebla, Puebla, Mexico

Back to Index