<%@LANGUAGE="VBSCRIPT" CODEPAGE="1252"%> Galo's Home Page IEURI/M Final Report

IUERI/M Final Report

Gabriel Corvera

Computer Science Department, Cornell University

and

Instituto Tecnológico y de Estudios Superiores de Monterrey

Campus Estado de México

This is the final report for the six-month research internship. In the following links you will find useful information about the implementation of WalkMinQBF, an Algorithm that showed to outperform the state of art QBF solvers on solving Random UNSAT QBF formulas. Also you will find some general information about heuristics, computer complexity, SAT, QBF and MINSAT.

The document explains the modifications made to WalkMINSAT, KCNFS, WalkQBF and how they are now integrated into a QBF solver. The data structures and algorithms details are also explained. At the end I give some ideas of future work that can be done.

This work is related to the paper "Finding small unsat cores to prove unsatisfiability of QBF's" accepted for the Ninth International Symposium on Artificial Intelligence and Mathematics.

Index

General Concepts

N-Queens and Pigeon Hole Problem

Conclusions and References

Main Downloads

WalkMINSAT	(ZIP)
WalkMinQBF	(TAR.GZ)
WalkMINSAT User's Manual	(HTML)
WalkMinQBF User's Manual	(HTML)
Quaffle Functions and Structures Guide	(HTML)
QBF Generator	(ZIP)