Eina educativa de suport per l'estudi de resoledors SAT

Abstract

A la Universitat de Girona s’ofereix el Grau en Enginyeria Informàtica on al quart curs els alumnes han d’escollir un dels 4 itineraris proposats. En l’itinerari Enginyeria de la Computació es cursa l’assignatura Programació declarativa. Aplicacions, on s’estudien varies tècniques per resoldre problemes combinatoris. Una d’aquestes tècniques és la reducció al problema de satisfactibilitat booleana o SAT, explicat més endavant. A part d’aprendre com reduir els problemes a SAT també s’estudia el funcionament dels solucionadors SAT i les tècniques que aquests solucionadors utilitzen. Entendre el funcionament dels solucionadors Conflict-Driven Clause-Learning (CDCL), especialment les tècniques de Clause learning i Backjumping, pot ser complicat al principi. L'objectiu del projecte és crear una eina de caràcter educatiu, interactiva i visual a disposició dels estudiants i el professorat per tal de facilitar l'estudi dels solucionadors SAT. S'han ajuntat els apartats d'anàlisi, disseny i implementació en un de sol perquè han estat molt relacionats en el desenvolupament i ha permès facilitar-ne la lectura

The University of Girona offers the Degree in Computer Engineering where in the fourth year the students must choose one of the 4 itineraries proposed. In the Computer Engineering route, the subject Declarative Programming is studied. Applications, where various techniques are studied to solve combinatorial problems. One of these techniques is the reduction to the Boolean satisfiability problem or SAT, explained later. Apart from learning how to reduce the problems in SAT, we also study the operation of the SAT solvers and the techniques these solvers use. Understand how Conflict-Driven Clause-Learning (CDCL) solvers work, especially Clause learning and Backjumping techniques, it can be complicated at first. The aim of the project is to create an educational, interactive and visual tool available of students and faculty in order to facilitate the study of SAT solvers. The analysis, design and implementation sections have been combined into one because they have been very related in development and has made it easier to read