The SAT problem its one of the most challenging computer science open problems. I’m passionate about it, since my first steps in algorithms at programming challenges, and after at my degree thesis.

At thesis, i developed the next version of Demuba, a automatic demonstrator designed firstly by the Professor and Researcher Ricardo Oscar Rodriguez. The new version introduces a heuristic for guidance the selection of formula’s to get a refutation, if exists, in less time. This heuristic was designed by combining different approach to solve SAT problem. This solution its extensively specified in the thesis document.

Once finished the formal steps of thesis, i started my own method for SAT solving. I work on it at my free time, this is a private project.