Adaptar MiniSAT per un 3-SAT per resoldre Nonogrames

Abstract

La resolució de problemes de satisfacció booleana, coneguts comunament com a problemes SAT (de Boolean Satisfiability Problem en anglès), és una de les àrees més estudiades en la teoria de la computació i en la lògica. En les darreres dues dècades SAT ha esdevingut estat de l’art pel que fa a eina per a resoldre problemes combinatoris. Un Nonograma és un problema combinatori en forma de trencaclosques lògic en què el jugador ha de pintar o deixar en blanc les cel·les d’una graella segons les pistes numèriques donades per cada fila i columna. Aquestes pistes indiquen les seqüències de cel·les negres consecutives, però no especifiquen la seva posició exacta. El repte consisteix a deduir la configuració correcta de la graella, la qual revela habitualment una imatge oculta. Aquest treball se centra en dos objectius principals: la implementació d’un sistema d’anàlisi de clàusules específiques, tant abans d’iniciar la cerca com durant, dins del SAT solver MiniSAT, i la identificació de codificacions eficients per a Nonogrames que puguin beneficiar la seva resolució. L’objectiu d’aquest treball és analitzar les diferents codificacions per a Nonogrames i com l’activació de diversos anàlisis impactava en la seva resolució.

9