Pràctica 1: SAT solver

Modifica el SAT solver SAT-alumnes.cpp per a tractar de la manera més eficient que puguis els exemples de random3SAT.tar.gz. Teniu una presentació descrivint l’algorisme aquí, amb l’exemple en format DIMACS pel SAT solver.

Per a aconseguir això, millora l’heurística de decisió i la velocitat de propagació:

1. Propagació.

   A cada volta del bucle de propagateGivesConflict, cal propagar que modelStack[indexOfNextLiteralToPropagate] s’ha tornat cert.

   Per fer-ho, podeu fer servir occur lists: per cada literal l, tenim una llista occurList[l] que conté els índexs de les clàusules on apareix l.

   Quan cal propagar que un literal l és cert, el que fem és visitar les clàusules de occurList[-l] i mirem si n’hi ha cap que s’hagi tornat falsa (conflicte!) o unitària (propagació!).
2. Heurística de decisió.

   1. Tenim, per cada variable, un comptador del nombre de clàusules on apareix.

      En getNextDecisionLiteral, quan hem de decidir, escollim la variable indefinida amb aquest comptador més alt.
   2. Tenim, per cada variable, un comptador del nombre de conflictes en què ha aparegut. Quan hem de decidir, escollim la variable indefinida amb aquest comptador més alt.

      Una millora que es pot fer és donar més pes als conflictes recents. Per exemple, cada X conflictes, dividim els comptadors per la meitat.

Adjuntem un script que compara l’eficiència del teu solver amb un altre, kissat, executant tots dos en la mateixa màquina. Sobre els problemes insatisfactibles de 300 variables, kissat mai hauria de ser més de 20 vegades més ràpid que el teu solver, i és perfectament possible aconseguir ràtios de 10 vegades, 5 vegades, o fins i tot millors (fes make usant el Makefile per a compilar).

Has de lliurar dos arxius: SAT-alumnes.cpp i temps.txt, la sortida que genera l’script.