The problem of deciding the satisfiability of propositional formulas (SAT) does not only lie at the heart of the most important open problem in complexity theory (P vs.~NP), it is also at the basis of many practical applications in such areas as Electronic Design Automation, Verification, Artificial Intelligence, and Operations Research. Thanks to recent advances in SAT-solving technology, propositional solvers are becoming the tool of choice for attacking more and more practical problems. Timetabling problems are, in general, NP problems , hence, an encoding may be found to SAT. In this document we present work done in developing different encodings of three cases of timetabling problems to SAT, namely one school timetabling specific case and two formulations for university timetabling. We show that these encodings may be a good solution aproach for real-world problems that need a zero-cost solution.

Es conocido que muchos problemas de eneración de horarios (problemas de Timetabling) son NP-completos; sin embargo, existe gran interés en investigarlos ya que son problemas que emergen de necesidades reales y de amplia aplicación práctica. En este sentido, varios enfoques han sido propuestos como solución (al menos parcial) a este tipo de problemas. A pesar de ello, la comunidad que los investiga ha prestado poca atención a la posibilidad de reducir (aprovechando su NP-Completitud) estos problemas a otros relacionados en los que se hayan reportado buenos resultados. Tal es el caso del problema de satisfactibilidad de fórmulas lógicas proposicionales SAT. Problema sobre el cual, en los últimos años, se han suscitado avances considerables con capacidad de decidir fórmulas lógicas proposicionales de decenas de miles de variables y millones de cláusulas. Aprovechando esto, se ha explorado la aplicabilidad de reducir problemas de timetabling a SAT. Para ello, se han implementado varios programas que tomen como entrada un problema de timetabling y lo conviertan a un problema de SAT, de igual manera, se programaron las aplicaciones necesarias para reconvertir un modelo de la fórmula lógica proposicional a una solución para el problema original. A continuación se presenta un resumen sobre las experiencias obtenidas sobre tres tipos distintos de problemas sobre generación de horarios. Primero, se presentan generalidades sobre SAT y algunas consideraciones sobre la reducción de problemas a éste. Directamente después se presentan las distintas reducciones probadas así como los resultados obtenidos y conclusiones preliminares sobre la pertinencia de este enfoque.