| Popis: |
Advancements in SAT solving algorithms with heuristics and more sophisticated inferring techniques have allowed a wide array of real world applications for SAT solvers to prosper. In this work, an All-SAT solver based on the DPLL algorithm has been developed, optimized, and ultimately parallelized, with the objective of learning about the intricacies of SAT solvers from a performance engineering perspective. Ultimately, as a result of this work, a correct and complete parallel All-SAT solver, based on task-parallelism and a divide-and-conquer paradigm, has been successfully implemented and tested with a set of benchmark satisfiability problems. Avanços en els algoritmes per a la resolució del problema SAT amb heurístiques i tècniques d'inferència més sofisticades han permès que prosperi una àmplia gamma d'aplicacions en el món real per als solucionadors SAT. En aquest treball, s'ha desenvolupat, optimitzat i finalment paral·lelitzat un solucionador All-SAT basat en l'algorisme DPLL, amb l'objectiu de conèixer les complexitats dels solucionadors SAT des d'una perspectiva d'enginyeria del rendiment. En última instància, com a resultat d'aquest treball, s'ha implementat amb èxit un solucionador All-SAT paral·lel correcte i complet, basat en el paral·lelisme de tasques i el paradigma divideix-i-venceràs, testejat amb un conjunt de problemes de satisfacibilitat de referència. Avances en los algoritmos para la resolución del problema SAT con heurísticas y técnicas de inferencia más sofisticadas han permitido que prospere una amplia gama de aplicaciones en el mundo real para los solucionadoes SAT. En este trabajo, se ha desarrollado, optimizado y finalmente paralelizado un solucionador All-SAT basado en el algoritmo DPLL, con el objetivo de conocer las complejidades de los solucionadores SAT desde una perspectiva de ingeniería del rendimiento. En última instancia, como resultado de este trabajo, se ha implementado con éxito un solucionador All-SAT paralelo, correcto y completo, basado en el paralelismo de tareas y el paradigma de divide-y-vencerás, testeado con un conjunto de problemas de satisfacibilidad de referencia. |
