Fase 2 del Proyecto
Contents
1. algunas mejoras a nivel de implementaci n como el reemplazo de los arreglos contiguos en memoria por listas enlazadas permitiendo un aprovechamiento mejor de la memoria disponible y apuntadores a los elementos necesarios cuando el orden de acceso deba ser constante Ya se implement una primera aproximaci n a esta idea con la lista de cl usulas aprendidas Referencias Bibliogr ficas 1 Joao P Marques Silva y Karem A Sakallah GRASP A New Search Algorithm For Satisfiability 2 Mathew W Moskewicz Conor F Madigan Ying Zhao Lintao Zhang y Sharad Malik Chaff Engineering An Efficient SAT Solver 3 Lintao Zhing y Sharad Malik The Quest For Efficient Boolean Satisfiability Solvers2. Sin embargo todos est n basados en el algoritmo DPLL Davis Putnam Logemann Loveland que sigue la siguiente estructura b sica DPLL inicializar_entorno if estado DESCONOCIDO return estado while true I if Idecidir proxima variable I if No se puede deshacer return INSATI SFACI BLE while true estado deshacer if estado INSATISFACIBLE return INSATI SFACI BLE else if estado SATISFECHO return SATI SFECHO else if estado DESCONOCIDO break empilar_evento Asignacion de Decision estado asignar_variable if estado SATISFECHO return SATISFECHO else if estado CONFLICTO I if No se puede deshacer return INSATISFACIBLE while true estado deshacer if estado INSATISFACI BLE return INSATI SFACI BLE else if estado SATISFECHO return SATI SFECHO else if estado DESCONOCIDO break while true estado propagar if estado CONFLICTO if No se puede deshacer return INSATI SFACI BLE while true estado deshacer if estado INSATISFACI BLE return INSATI SFACI BLE else if estado SATISFECHO return SATI SFECHO else if estado DESCONOCIDO break else if estado SATISFECHO return SATISFECHO else break Figura 1 Algoritmo DPLL De c mo se implementen las funciones decidir_proxima_variable y deshacer depender el funcionamiento del algoritmo Por ejemplo el algoritmo DPLL original puede obtenerse haciendo que
3. aprendizaje es id ntico al Simple en cuanto a la heur stica de decisi n y la manera de deshacer cuando hay conflicto La nica diferencia es a nivel de concepto en implementaci n es id ntico que cuando ocurre un conflicto y la ltima variable de decisi n es asignada el complemento de su valor actual a manera de propagaci n se hace como consecuencia de lo que arrojar a el BSP sobre la nueva cl usula aprendida La segunda versi n es equivalente a su vez a la que implementa la heur stica de decisi n del GRASP LA tercera y ltima versi n implementa la heur stica de decisi n que proponen los creadores de chaff Dicha decisi n est basada en una heur stica que ellos llaman VSIDS Variable State Independant Decaying Sum en donde para cada variable y cada polaridad se mantiene un contador que est activo durante toda la ejecuci n del programa Cada vez que se aprenda una cl usula nueva a cada variable que participe de dicha cl usula se le incrementa el contador en su polaridad correspondiente De esta manera se escoge siempre la variable y polaridad con el contador m s elevado De igual manera peri dicamente se debe ir dividiendo el valor de todos los contadores por una cierta constante Como ya se mencion antes el valor que se suma a los contadores es uno 1 la constante que divide es dos 2 y la periodicidad es siempre que se asigne una nueva variable de decisi n La raz n por la que sta es una buena heur stica es
4. de SAT utilizadas para poner a prueba los revolvedores actualmente pueden tener millones de variables y miles de millones de cl usulas Nuestra sospecha respaldada por el esfuerzo que hacen la mayor a de los revolvedores eficientes actuales es que para estas instancias de SAT gigantes no basta solo BSP Entonces se decidi incorporar algunas de las t cnicas modernas para revolvedores de SAT como lo son una heur stica de decisi n se decide que variable entre las libres se va a asignar en cada momento basado en alguna funci n de conveniencia el backtracking no cronol gico se permite retroceder m ltiples niveles en la recursi n y el aprendizaje de cl usulas se permite la incorporaci n de cl usulas que son redundantes a la formula original pero pueden ayudar a encontrar implicaciones antes ignoradas En el presente informe se exponen con m s detalle las t cnicas implementadas En primer lugar el dise o general de la aplicaci n Estructuras de datos y algoritmos utilizados luego los detalles de la implementaci n instrucciones para la operaci n de la aplicaci n una breve descripci n del estado actual del programa y terminando con algunas conclusiones y recomendaciones para trabajo futuro Dise o de la aplicaci n Con fines de comparaci n se han implementado varios revolvedores SAT diferentes que difieren entre s en uno o varios aspectos como la heur stica de decisi n o la incorporaci n de aprendizaje
5. por que se va a intentar primeramente asignar las variables que ocasionaron el conflicto en direcci n a no volver a ocasionarlo El mayor problema encontrado a la hora de la implementaci n fue en realidad al intentar continuar con esta fase del proyecto partiendo de lo que fue la primera entrega lo cual nos fue imposible Es por esto que se decidi primero re implementar de otra manera el equivalente a la primera fase del proyecto Esto nos permiti luego poder implementar las heur sticas de decisi n el bactracking no cronol gico de manera relativamente r pida sin embargo la re implementaci n de dicha primera fase tom una cantidad considerable de tiempo para que funcionara como nosotros quer amos Instrucciones de operaci n La aplicaci n completa en todas sus versiones deber copiarse en un mismo directorio Desde la consola del sistema en el directorio donde se coloc la aplicaci n se debe ejecutar la instrucci n make la cual se encarga de compilar todos los elementos necesarios de la aplicaci n Para ejecutar cualquiera de las diferentes versiones se debe cambiar de directorio al que corresponda a la versi n deseada y ejecutar una instrucci n de la forma proyecto II lt archivo de entradas lt plantilla de salida gt donde lt archivo de entradas es un archivo que contenga un conjunto de instancias de SUDOKU en el formato acordado y lt plantilla de salida gt es un trozo de nombre da archivo que se va a u
6. que este es exactamente el comportamiento que tiene el backtracking no cronol gico sin siquiera la necesidad de guardar un nivel para cada evento ni guardar de manera expl cita un grafo de implicaciones para calcular a que nivel se debe saltar El aprendizaje de cl usulas es como el propuesto para GRASP se toman todas las variables asignadas por una decisi n anteriores a la ocurrencia del conflicto y se agrega una nueva cl usula conformada por el complemento de cada una de dichas asignaciones N tese ahora que cuando deshacer empila la segunda rama de b squeda de una variable de decisi n como una asignaci n de propagaci n no lo hace sin sentido ya que en la cl usula nueva la ultima variable de decisi n es precisamente la nica que quedar a sin asignar y por BSP su valor es implicado Detalles de la implementaci n Como se ha dicho anteriormente con fines de comparaci n se han implementado un conjunto de resolvedores SAT todos basados en el algoritmo DPLL pero que difieren en algunos aspectos como la heur stica de decisi n de variables libre o la incorporaci n de un sistema de aprendizaje de cl usulas En primer lugar se implement una versi n Simple que emula el comportamiento del algoritmo DPLL original BCP y corresponde a la re implementaci n de la primera fase del proyecto En esta versi n la funci n que decide que variable libre ha de ser la pr xima a asignar toma la primera variable libre sin asi
7. 09 seg 0 115 seg O min O min O min O min O min O min 0 114 seg 0 115 seg 0 113 seg 0 108 seg 0 108 seg 0 114 seg 0 min O min O min O min O min 0 min 0 112 seg 0 439 seg 0 106 seg 0 107 seg 0 104 seg 0 112 seg 0 min O min O min O min O min 0 min 0 114 seg 0 111 seg 0 107 seg 0 108 seg 0 105 seg 0 114 seg 0 min O min O min O min O min O min 0 112 seg 0 111 seg 0 107 seg 0 105 seg 0 104 seg 0 112 seg O min O min O min O min O min 0 min 0 112 seg 0 109 seg 0 106 seg 0 119 seg 0 104 seg 0 112 seg O min O min 0 min 0 min O min O min 0 135 seg 0 111 seg 0 107 seg 0 105 seg 0 108 seg 0 135 seg 0 min 0 min 0 min 0 min O min 0 min 0 114 seg 0 113 seg 0 111 seg 0 107 seg 0 104 seg 0 114 seg 0 min 0 min 0 min O min O min 0 min 0 115 seg 0 112 seg 0 108 seg 0 108 seg 0 109 seg 0 115 seg 0 min O min O min 0 min O min O min 0 111 seg 0 122 seg 0 108 seg 0 106 seg 0 107 seg 0 111 seg O min O min 0 min OU min O min O min 0 114 seg 0 114 seg 0 112 seg 0 110 seg 0 109 seg 0 114 seg 0 min 0 min O min O min O min 0 min 0 113 seg 0 108 seg 0 108 seg 0 106 seg 0 106 seg 0 113 seg 0 min 0 min O min O min O min O min 0 118 seg 0 112 seg 0 121 seg 0 109 seg 0 105 seg 0 118 seg 0 min 0 min O min O min 0 min O min 0 110 seg 0 111 seg 0 107 seg 0 104 seg 0 103 seg 0 110 seg 0 min O min O min O min 0 min O min 0 111
8. 19 seg 113 seg 113 seg 0 min O min O min O min O min 0 min 111 seg 114 seg 110 seg 111 seg 107 seg 111 seg 0 min 0 min O min O min O min 0 min 126 seg 897 seg 122 seg 890 seg 107 seg 126 seg O min O min O min O min O min 0 min 110 seg 264 seg 110 seg 198 seg 125 seg 110 seg 0 min O min E MA MEN NE Seg seg g 552 seg 0 min ml O min O min 0 min 114 seg 118 seg p 155 seg 114 seg O min 0 min O min O min O min 0 min 135 seg 167 seg 142 seg 155 seg 111 seg 135 seg 0 min pr 0 min 1 min O min 0 min 451 seg Sea 449 seg 268 seg 305 seg 451 seg O min 0 min 0 min O min 0 min O min 119 seg 172 seg 116 seg 170 seg 115 seg 119 seg 0 min O min O min O min O min O min 111 seg 169 seg 117 seg 142 seg 111 seg 111 seg O min 0 min O min O min O min 0 min 114 seg 177 seg 113 seg 163 seg 108 seg 114 seg 0 min O min O min O min O min 0 min 118 seg 205 seg 180 seg 197 seg 111 seg 118 seg 0 min O min O min O min O min 0 min 109 seg 161 seg 104 seg 148 seg 113 seg 109 seg 0 min O min O min O min O min O min 118 seg 132 seg 111 seg 124 seg 109 seg 118 seg 0 min O min O min O min 0 min 0 min 116 seg 197 seg 109 seg 182 seg 119 seg 116 seg 0 min O min O min O min 0 min O min 121 seg 170 seg 122 seg 168 seg 114 seg 121 seg 0 min E O min O min 0 min 143 seg 136 seg E 114 seg 143 seg 0 mi
9. O min 0 min O min O min O min 0 112 seg 0 202 seg 0 104 seg 0 136 seg 0 126 seg 0 112 seg Como se puede ver se obtuvieron para el resolvedor Simple y Aprendizaje Heur stica Chaff esto se debe en gran medida a que para todas las versiones se implement un mecanismo de backtracking no cronol gico en el caso de Simple no existe ning n overhead por incluir las t cnicas propuestas y en el caso de Aprendizaje Heur stica Chaff la combinaci n de las t cnicas junto con una heur stica que funciona muy bien compensa dicho overhead Para ambos caso en los que se implement la heur stica de GRASP se tienen casos que no corren a tiempo y los dem s tienden a correr un poco m s lento Esto se debe a la incorporaci n de una heur stica de decisi n que probablemente no sea adecuada para la estructura y el tama o de las formulas CNF proporcionadas La versi n Aprendizaje Simple funciona casi tan bien como las dos nombradas primeramente sin embargo los tiempos de ejecuci n ligeramente mayores se deben al overhead que implica el aprendizaje de cl usulas que sin una buena heur stica que aproveche dicho aprendizaje se hace apreciable Estamos satisfechos con los resultados obtenidos por nuestro resolvedor que por lo menos para las instancias de SAT proporcionada se comporta de manera competitiva con el resolvedor zchaff considerado como uno de los actuales revolvedores del estado del arte Sin embargo a n podr an incorporare
10. Universidad Sim n Bol var Sede De Sartenejas Departamento de Computaci n y Tecnolog a de la Informaci n C1 5651 Dise o de Algoritmo I Enero Marzo 2008 Fase 2 del Proyecto BSP Heur stica de Decisi n Backtracking No Cronol gico y Aprendizaje Profesor Integrantes Oscar Meza Ricardo Monascal 03 36207 Cristina Sanju n 03 36486 Introducci n En la primera fase del proyecto se implement un resolvedor de SAT con el objetivo de resolver instancias de SUDOKU por medio de una reducci n de cada una de estas instancias a una instancia de SAT Dicho resolvedor era capaz de resolver una cantidad grande de los casos de pruebas a los que fue expuesto sin embargo hubo instancias que el resolvedor no pudo manejar en un tiempo razonable Realizando una revisi n m s profunda del anterior proyecto y re implementandolo de una nueva manera se logr correr todos los casos en un tiempo mucho menor a un segundo comparable con los tiempos obtenidos por el resolvedor zchaff El resolvedor hasta el punto de la entrega pasada estaba basado en el algoritmo DPLL incluido el an lisis de implicaciones o Boolean Constraint Propagation Los resultados obtenidos con este enfoque re implementado apuntan a que dicha organizaci n es suficiente para obtener buenos resultados con instancias de SAT tan peque as Para un SUDOKU cl sico la reducci n arroja 729 variables y un poco mas de 11988 cl usulas Hay que recordar que las instancias
11. _CLAUSULA que recordemos es cuando se ha satisfecho una cl usula En las dos versiones anteriores los eventos de tipo SAT_CLAUSULA ten an en el ndice el ndice de la cl usula en el orden en que fue le da del archivo En atenci n a que ahora existen dos estructuras de datos que contienen cl usulas y una de ellas no tiene acceso de tiempo constante Para alcanzar el i simo elemento de una lista hay que pasar necesariamente por los primeros i 1 se asigna como ndice del evento la direcci n de memoria de dicha cl usula Esto hace que la estructura en la que se encuentra la cl usula satisfecha es indiferente y el acceso a cualquiera de dichas cl usulas es constante N tese que en las funciones de propagaci n que implementa BSP incluyendo calcular los efectos de una asignaci n espec fica de una variable la b squeda de una cl usula unitaria entre otros el acceso a la lista de cl usulas es lineal ya que deben recorrerse todas las cl usulas Sin embargo una estructura de tipo lista es ideal para secuencias de objetos a los que se les va accediendo en un determinado orden El tama o de las cl usulas aprendidas en otras palabras la cantidad de variables que incluyen es ilimitado De todas formas la cl usula m s grande posible solo tendr a 729 variables La cantidad de cl usulas que pueden ser aprendidas es tambi n ilimitada dependiente nicamente de la cantidad de memoria disponible La primera versi n que incluye
12. alto Con el objetivo de evitar el elitismo de variables que fueron muy utilizadas y luego ya no se dividen peri dicamente todos los contadores por alguna constante En nuestro caso el valor que sumamos es uno 1 y la constante por la que dividimos es dos 2 Dado el corto tiempo de ejecuci n para estas instancias peque as de SAT se divide siempre que se decida el valor de una nueva variable Cambios en estas constantes produjeron resultados id nticos as que nos quedamos con uno solo La funci n deshacer influye tambi n mucho en el funcionamiento del resolvedor De aqu viene la raz n por la que solo hace falta asignarle a una variable un valor por decisi n no propagaci n en uno solo de sus dos valores posibles La funci n deshacer deshace asignaciones de propagaci n y satisfacciones de cl usulas hasta que se consiga una asignaci n de decisi n En este momento la misma funci n de deshacer puede asignar a la variable el valor contrario al que ten a si no hab a agotado ya sus opciones y empilar un nuevo evento de asignaci n por decisi n Sin embargo se puede introducir el backtacking no cronol gico a esta estrategia con muy poco esfuerzo En vez de empilar el valor contrario de la variable como otra decisi n se empila como una propagaci n m s de esta manera la pr xima vez que se llame a deshacer esta asignaci n ser deshecha y se seguir deshaciendo hasta encontrar alguna asignaci n de decisi n N tese
13. decidir_proxima_variable retorne siempre la ultima variable que no ha agotado sus dos asignaciones posible y que deshacer solo deshaga las implicaciones ocurridas por asignaciones un nivel inmediatamente anterior En cuanto a las estructuras de datos para cada variaci n de la aplicaci n en general se conserva un tipo de datos cl usula que tiene la cantidad de variables en dicha cl usula un arreglo con los ndices de las variables pertenecientes a dicha cl usula la cantidad de variables que quedan sin asignar y si dicha cl usula ya ha sido satisfecha o no Para las variables no se tiene una estructura de datos especial sino solo un arreglo de enteros que representa el valor de la asignaci n de dicha variables que puede ser TRUE FALSE o SIN_ASIGNAR Para el manejo de la pseudo recursi n que se implementa de manera iterativa se tiene una pila de eventos donde cada evento tiene un tipo un ndice y un valor Los eventos pueden ser de tipo ASIG_BACKTRACK que equivale a una decisi n sobre una variable libre de tipo ASIG_PROPAGACION que equivale a la asignaci n de una variable en respuesta a una implicaci n del BSP En ambos casos el ndice del evento es el ndice de la variable asignada y el valor del evento el valor que le fue asignado Un evento tambi n puede ser de tipo SAT_CLAUSULA que equivale a la satisfacci n de una determinada cl usula en cuyo caso el ndice del evento dependiendo de si el aprendizaje de cl u
14. gnar ordenadas por su ndice o etiqueta La funci n que deshace implementa un pseudo bactracking no cronol gico donde se aplica la misma t cnica explicada anteriormente para dicha t cnica con la salvedad de que no se aprenden cl usulas de conflictos De esta manera la asignaci n de propagaci n que se hace con la ltima variable asignada por su valor complemento no proviene del resultado de un BSP sino de la incorporaci n de una regla nueva Si se llega a un conflicto la ltima variable asignada como m nimo es incorrecta por lo tanto debe implicarse que dicha variable adopte el valor de su complemento En segundo lugar para otra versi n se incorpor una heur stica de decisi n diferente En este caso se incorpor la misma heur stica que se utiliza en el resolvedor GRASP la cual consta de lo siguiente Se calcula para cada variable y cada polaridad la cantidad de cl usulas que quedar an directamente satisfechas al asignar a dicha variable la polaridad correspondiente Se escoge la variable y polaridad con el mayor valor que satisfaga directamente la mayor cantidad de cl usulas La funci n que deshace es la misma que se describi para de caso Simple Luego se tienen tres versiones adicionales que incorporan el aprendizaje de cl usulas Las cl usulas aprendidas se guardan en una lista aparte de las cl usulas originales le das del archivo CNF en atenci n a este cambio de estructura cuando ocurre un evento de tipo SAT
15. n O min 0 min 0 min O min 0 min 119 seg 218 seg 116 seg 212 seg 115 seg 119 seg 0 min B O min O min O min 266 seg 256 seg z 423 seg 266 seg O min S O min o O min O min 158 seg 153 seg 113 seg 158 seg 0 min O min O min O min O min 0 min 109 seg 128 seg 106 seg 120 seg 112 seg 109 seg 0 min O min O min O min O min 0 min 109 seg 132 seg 105 seg 126 seg 114 seg 109 seg O min O min O min O min O min 0 min 110 seg 132 seg 105 seg 125 seg 115 seg 110 seg 0 min O min 0 min O min O min 0 min 117 seg 503 seg 113 seg 507 seg 116 seg 117 seg 0 min O min 0 min O min O min 0 min 0 111 seg 0 119 seg 0 111 seg 0 113 seg 0 108 seg 0 111 seg 0 min O min O min O min O min O min 0 131 seg 0 520 seg 0 119 seg 0 505 seg 0 115 seg 0 131 seg 0 min O min O min 0 min O min O min 0 114 seg 0 181 seg 0 144 seg 0 172 seg 0 118 seg 0 114 seg 0 min O min O min O min O min 0 min 0 110 seg 0 297 seg 0 115 seg 0 287 seg 0 125 seg 0 110 seg 0 min O min O min O min O min 0 min 0 112 seg 0 146 seg 0 259 seg 0 135 seg 0 116 seg 0 112 seg O min O min O min O min O min 0 min 0 114 seg 0 293 seg 0 159 seg 0 258 seg 0 114 seg 0 114 seg 0 min O min O min O min 0 min 0 min 0 140 seg 0 413 seg 0 106 seg 0 395 seg 0 106 seg 0 140 seg 0 min
16. seg 0 113 seg 0 105 seg 0 105 seg 0 104 seg 0 111 seg O min O min 0 min O min O min 0 min 0 139 seg 0 119 seg 0 108 seg 0 103 seg 0 105 seg 0 139 seg O min O min 0 min 0 min 0 min 0 min 0 109 seg 0 110 seg 0 106 seg 0 106 seg 0 104 seg 0 109 seg O min O min O min O min O min 0 min 0 111 seg 0 113 seg 0 105 seg 0 105 seg 0 105 seg 0 111 seg O min O min O min O min O min O min 0 111 seg 0 113 seg 0 108 seg 0 105 seg 0 104 seg 0 111 seg 0 min O min O min O min O min O min 0 121 seg 0 236 seg 0 117 seg 0 230 seg 0 107 seg 0 121 seg 0 min O min O min O min O min 0 min 0 120 seg 0 206 seg 0 118 seg 0 196 seg 0 117 seg 0 120 seg O min O min O min O min O min 0 min 0 113 seg 0 282 seg 0 112 seg 0 281 seg 0 106 seg 0 113 seg 0 min O min O min O min O min 0 min 0 116 seg 0 214 seg 0 112 seg 0 208 seg 0 118 seg 0 116 se 0 min 0 min 0 min 0 min O min O min 120 seg 165 seg 116 seg 160 seg 109 seg 120 seg O min Y O min O min 0 min 163 seg 160 seg z 824 seg 163 seg 0 min O min O min 0 min O min O min 120 seg 153 seg 116 seg 148 seg 109 seg 120 seg 0 min O min O min O min O min 0 min 113 seg 124 seg 109 seg 1
17. sulas est activado o no es el ndice de la cl usula en cuesti n la direcci n de memoria de la misma el valor del evento es irrelevante En el caso en el que el aprendizaje de cl usulas est activado se guardan las cl usulas aprendidas en una lista independiente del conjunto de cl usulas originales por esto es importante que se empile la direcci n de la cl usula y no su ndice Para la heur stica de decisi n se implementaron tres m todos El primero emula el comportamiento de la selecci n lineal es decir la escogencia de la primera variable no asignada con el valor FALSE luego se ver como se le asigna luego TRUE cuando la primera asignaci n lleva a un conflicto El segundo m todo es el propuesto por los creadores de GRASP el cual toma la variable y la polaridad tal que al asign rsele dicho valor satisfaga directamente la mayor cantidad de cl usulas El tercer m todo es el propuesto por los creadores de chaff que ellos denominan VSIDS Variable State Independant Decaying Sum para la cual es estrictamente necesaria la incorporaci n del aprendizaje de cl usulas A grosso modo dicho m todo lleva dos contadores por cada variable uno por cada polaridad y cada vez que se aprenda una nueva cl usula se le suma un determinado valor a cada variable que participe de la misma en su polaridad correspondiente A la hora de decidir la pr xima variable a asignar se toma aquella variable y polaridad que tenga el contador m s
18. tilizar para completar los nombres de los diferentes tipos de archivos de salida como son los tableros individuales lt plantilla de salida gt _ lt numero de instancia gt txt los tableros traducidos a SAT SAT_ lt plantilla de salida gt _ lt numero de instancia gt txt y los archivos de solucion tanto para nuestro resolvedor SATurn solucion_SATurn_ lt plantilla de salida gt _ lt numero de instancia gt txt como para el resolvedor de dominio p blico zchaff solucion zchaff lt plantilla de salida gt lt numero de instancia gt txt Para todos estos archivos lt numero de instancia gt es el orden de aparici n de dicho tablero de entre los tableros v lidos en lt archivo de entradas Estado Actual El estado actual de la aplicaci n es totalmente operativo o por lo menos no se encontr ning n caso para el cual la aplicaci n falle El nico problema viene dado con algunas instancias de tablero utilizadas que corren por demasiado tiempo en algunas de las versiones implementadas Conclusiones y recomendaciones Para esta fase del proyecto se implement una mejora al resolvedor SAT que se hab a entregado como primera fase las cuales incluyen heur sticas de decisi n backtracking no cronol gico y aprendizaje de cl usulas Sin embargo se ha demostrado que para las instancias peque as de SAT que genera la reducci n de un tablero cl sico 729 variables y un poco m s de 11988 cl usulas tomando en cuenta que los re
19. volvedores actuales resuelven instancias de SAT con millones de variables y miles de millones de cl usulas la incorporaci n de dichas t cnicas salvando el backtracking no cronol gico no muestra mejora alguna Este se debe a la estructura de la f rmula proporcionada y del overhead que implican dichas t cnicas A continuaci n se muestra una tabla con los tiempos de corrida para cada una de las versiones implementadas y zchaff tomando 60 casos de prueba repartidos en 6 niveles de dificultad Las corridas se hicieron en unas de las maquinas del Laboratorio Docente de Computaci n baraka tomando como timeout para las corridas 10 minutos Lo cual es razonable ya que los revolvedores actuales para resolver instancias gigantes de SAT utilizan un timeout que var a entre 1 2 hora y 3 horas Adem s como se podr ver en la tabla todas las versiones resuelven la instancia en menos de medio segundo o en m s de 10 minutos de lo que se puede intuir que probablemente dichas instancias se tarden incluso mucho m s que esta cota OS RA Aprendizaje Aprendizaje Simple dreg din Heur stica Heur stica zchaff asp omPie Grasp Chaff 0 min O min 0 min 0 min O min 0 min 0 118 seg 0 110 seg 0 113 seg 0 109 seg 0 107 seg 0 118 seg O min O min O min 0 min O min 0 min 0 115 seg 0 112 seg 0 110 seg 0 110 seg 0 1
Download Pdf Manuals
Related Search