información
Contents
1. 1 tal que la f rmula sea verdad 2 Diseno 2 1 Descripci n general del algoritmo empleado El programa propuesto sigue el esquema general del algoritmo DPLL que presentaron Martin Davis Hilary Putnam George Logemann y Donald Loveland para decidir el problema de satisfacci n booleana Seguidamente presentamos el esquema general del algoritmo DPLL que hemos adaptado de 4 status preprocess if status UNKNOWN return status while true Fase de seleccion de variable a asignar decide _next_branch while true Fase de deduccion status deduce if status CONFLICT conflict_result analyze_conflict if conflict_result 0 return UNSATISFIABLE else backtrack J else if status SATISFIABLE return SATISFIABLE else break Uno de los puntos en que esta presentaci n del algoritmo diverge del que presenta 4 es en el an lisis de conflicto y en la posibilidad de efectuar un backtracking no cronol gico En el programa que aqu describimos no se realiza sino una versi n muy simplificada de an lisis de conflicto en donde no hay aprendizaje de cl usulas y el backtracking se hace s lo de un nivel de decisi n en un nivel de decisi n cronol gico Entre las razones por las que se escogi el algorimo DPLL est n 1 Este algoritmo es la base para las implementaciones en los SAT solvers m s eficientes conocidos 2 El esquema general del algoritmo es bastante sencillo de2. 3 El campo propagated_var es la cabeza de una lista cuyos elementos son todas las variables booleanas 10 3 2 3 Ventajas de la implementaci n escogida para el backtrac king Entre las ventajas de la implementaci n iterativa para el backtracking est Resultar m s sencillo modificar el programa para implementar un bac tracking no cronol gico que si se hubiera implementado el backtracking de manera recursiva 3 2 4 Desventajas de la implementaci n escogida para el back tracking Quiz s la nica desventaja de la implementaci n iterativa respecto a la recursiva para el backtracking sea la mayor dificultad que supone el manejo expl cito de la pila que en el caso recursivo se maneja impl citamente con la pila de llamadas a subrutinas 4 Dificultades encontradas 5 Instrucciones de operaci n Para emplear la aplicaci n escribir en la consola el comando kec_o_sat_s f inputfilename o outputfilename donde inputfilename es el nombre del archivo que contiene la instancia del problema SAT a resolver Esta instancia debe estar en el formato DI MACS Consultar http logic pdmi ras ru basolver dimacs html pa ra informaci n sobre este formato outputfilename es el nombre del archivo que contendr los resultados generados tras correr el algoritmo Para m s detalles acerca de la operaci n leer el archivo README que se incluye con la distribuci n del programa 11 6 Estado Actual El
3. ndice 1 Introducci n 1 1 Motivaci n del proyecto En 1971 Stephen Cook propuso en su trabajo 1 una nueva categor a de complejidad de problemas de decisi n computacionales a la que llam pro blemas NP completos La caracterizaci n de esta categor a se hace sobre estas dos propiedades Todos los problemas NP completos pueden ser verificados en tiempo O p n donde p n es un polinomio en funci n de n el tama o de la instancia del problema Todos los problemas en NP pueden ser reducidos en tiempo O p n a alg n problema NP completo donde p n es un polinomio en funci n de n el tama o de la instancia del problema que es reducido Ahora bien fueron Cook y Leonid Levin quienes encontraron de for ma independiente el primer problema en esta categor a NP completos el problema de la satisfacci n booleana SAT Un a o despu s Richard Karp identific otros 21 problemas en esta categor a 2 los cuales ten an la no toria caracter stica de que para ellos no se conoce un algoritmo polinomial en funci n del tama o de la instancia que les de soluci n una cualidad que comparten todos los problemas en esta clase junto al hecho de que todos estos problemas ocurren con una marcada frecuencia en el rea de la compu taci n Sin embargo la caracter stica m s especial de stos es el segundo tem de arriba encontrar un algoritmo polinomial para tan s lo uno de ellos es encontrar un algoritmo polinomial para to
4. n se escogi la implementaci n de los 2 watched literals descrita en las fuentes 3 4 y y que fue propuesta con el programa 2Chaff Las razones para escoger esta implementaci n de 2 watched literals para la identificaci n de cl usulas unitarias son las siguientes 1 En pruebas de ejecuci n 4 se ha observado que el comportamiento de la implementaci n por 2 watched literals requiere de menor tiempo que implementaciones como la de SATO implementaci n a la que 4 se refiere como Head Tail lists y considerablemente menor tiempo que la implementaci n por contadores 2 La implementaci n de 2 watched literals no requiere que se realicen ope raciones sobre los watchers o sobre el conjunto de datos que permite directamente determinar cu les son las cl usulas unitarias cuando se realiza el backtracking a un nivel de decisi n anterior Las implemen taciones de SATO y contadores s requieren estas operaciones Esta ventaja es se alada por el trabajo 3 Entre las desventajas que trae consigo la implementaci n de 2 watched literlas est 1 Cuando es necesario mover alguno de los watchers porque la variable a la que apuntan en la cl usula resulta asignada se debe buscar una nueva variable no asignada puede que ni exista tal variable en la misma cl usula Entonces en el peor caso para identificar una cl usula unitaria la implementaci n de 2 watched literals tendr que recorrer todos los literales de un
5. programa se encuentra totalmente operativo 7 Conclusiones y recomendaciones Referencias 1 Cook Stephen The complexity of theorem proving procedures ACM 1971 2 Karp Richard Reducibility Among Combinatorial Problems Com plexity of Computer Computations 1972 ACM 1971 3 Lynce I y Marques Silva J Efficient Data Structures for Fast SAT Solvers Reporte T cnico Cadence European Laboratories Instituto de Engenharia de Sistemas e Computadores 2001 4 Zhang Lintao y Malik Sharad The Quest for Efficient Boolean Satis fiability Solvers 5 Zhang Lintao Searching for truth Techniques for satisfiability of boo lean formulas Tesis de doctorado Princeton University 2003 LA
6. se incurrir a en un costo adicional en comparaci n con la alternativa de tener a sat_st como variable global por la indirecci n que es necesario ejecutar en cada subrutina por cada vez que se quiera acceder a los campos de esta variable 3 1 Descripci n de la implementaci n de las cl usulas Para la implementaci n de cada cl usula se defini el siguiente tipo de dato clause typedef struct clause int size variablex head_watcher variable tail_watcher variablex literals clause IV ase la secci n 3 2 1 que describe la arborescencia impl cita que se recorre en el backtracking que a continuaci n describiremos campo por campo 1 Los apuntadores head_watcher y tail_watcher se alan cu les son los literales testigos watched literals de una cl usula En virtud de que en la fase de propagaci n de restricciones booleanas se opt por implementar la propagaci n de cl usulas unitarias con los 2 watched literals seg n se describe en 4 cada cl usula exige dos apuntadores a variables en la misma cl usula 2 Como cada cl usula es una disjunci n de literales optamos por repre sentarla como un arreglo de variables llamado literals Para poder recorrerlo es necesario almacenar su tama o que estar almacenado en el campo size de la cl usula 3 1 1 Ventajas de la implementaci n escogida para las cl usulas La implementaci n de los literales que componen una cl usula en un arreglo de vari
7. se describe se opt por por los cam pos pos_watched_list y neg watched list en el tipo SAT_status Cada uno de stos es un arreglo de cabezas de listas de forma que pos watched list lil sea la cabeza de la lista cuyos elementos son las cl usulas en las que el literal z ocurre como watcher An logamente ocurre con neg watched_list i es la cabeza de la lista cuyos ele mentos son las cl usulas en las que el literal 7 ocurre como watcher El campo model del tipo SAT_status es un arreglo de enteros tal que model 1 es el valor de asignaci n que se prueba para la variable x El model indica cu l nodo de la arborescencia del backtracking se est con siderando en un determinado instante de la ejecuci n Se incluye el campo num_clauses en el tipo SAT_status para poder recorrer el arreglo formula de todas las cl usulas que componen la f rmula A continuaci n comentaremos algunos detalles sobre la variable global sat_st La raz n por la que se escogi a sat_st de tipo SAT_status co mo variable global en lugar de pasarla como par metro entre las sucesivas llamadas a funciones durante la ejecuci n del algoritmo son 1 El pasaje del par metro sat_st a cada una de las funciones supone un costo acumulado muy grande a lo largo de la ejecuci n de todo el programa Cuando bien pudiera ahorrarse la operaci n de empilar esa par metro en cada llamada 2 Si se pasara una referencia a sat_ st como par metro a cada funci n
8. 1 0 asignado Imponemos adicionalmente una condici n a los nodos de esta arborescencia y es que la asignaci n hecha a las variables del nodo 2 7 no haga que la f mula no se pueda satisfacer Las i denotan variables booleanas distintas Yk 1 n Ahora dado un nodo z B t B t B sus sucesores son todos los nodos de la forma z B zti B 7 B zti B El backtracking implementado busca encontrar en la arborescencia en caso de que exista un nodo de la forma z B z2 B n B y que se corresponde con una asignaci n de valores de verdad a todas las variables que hace que la f rmula dada sea satisfecha si n es el n mero total de variables booleanas 3 2 2 Estructuras de datos que apoyan la implementaci n del bac tracking El backtracking se implement iterativo en lugar de recursivo por los motivos que se se alan en la secci n 3 2 3 Para ello fue necesario trabajar expl citamente con una pila de elementos de un nuevo tipo de dato llamado decision_level_data Este tipo almacena la informaci n que caracterizan a cada nodo del rbol impl cito que se recorre en el backtracking y que deben 2En 4 les llaman niveles de decisi n ser conservados en caso de que el algoritmo se encuentre con un nodo parcial que no tiene sucesores esto es con un nodo xr B zta B i Bl
9. a misma cl usula en busca de esta variable no asignada 2 3 2 Eliminaci n de literales puros La eliminaci n de literales puros en una f rmula dada en forma normal conjuntiva consiste en ubicar primero cu les son las variables booleanas que s lo ocurren con una polaridad en la f rmula Ahora bien estos literales que ocurren con una nica polaridad en toda la f rmula no condicionan la satisfacci n de la f rmula es decir si se eliminaran todos los literales puros la f rmula resultante es satisfactible si y s lo si asignando a los literales puros los valores de verdad que los satisfagan se logra que la f rmula original lo sea Lo explicamos con un ejemplo En la f rmula siguiente F 1 V 2 V T3 A 11 V72 A 23 el nico literal puro es z de forma que F ser satisfactible si y s lo si asignando a x el valor de verdad se logra que F gt 12V23 A 72 A 23 sea satisfecha Para la implementaci n de este mecanismo de deducci n se hizo un re corrido por todas las cl usulas de la f rmula anotando cu l es la polaridad que se ha observado para cada literal Si en un momento del paseo por las cl usulas de la f rmula se encuentra con un literal que ocurre con una polari dad distinta a la ya observada anteriormente para ese literal se descarta que esa variable sea un literal puro Para m s detalles consultar m s adelante 3 Detalles de implementaci n La implementaci n de la propagaci n de cl usulas unita
10. ables apuntado por literals implica Una rapidez de acceso en tiempo constante a cada literal de la cl usula Hecho que resulta de particular utilidad en los recorridos a trav s de los literales de cada cl usula que son efectuados durante la detecci n de literales puros y durante la actualizaci n de los watchers o testigos que permiten identificar cl usulas unitarias Recuerde el lector que se ha mencionado en la secci n que una de las desventajas de las implementaci n por 2 watched literals es que en el peor caso hay que recorrer todos los literales de una cl usula para determinar si sta es unitaria o no Un ahorro de espacio para los apuntadores el cual ser a necesario si la conjunci n de literales en las cl usulas se implementara con una lista enlazada 3 2 Descripci n de la implementaci n del Backtrac king 3 2 1 rbol impl cito del Backtracking Toda implementaci n de Backtracking es un recorrido Depth First Search sobre una arborescencia impl cita Esta descripci n impl cita de la arbores cencia a recorrer exige que se defina cu les son sus nodos y para cada nodo cu les son sus nodos sucesores En el caso que nos concierne los nodos son de la forma Bo B i B Tip Z B donde 0 lt k lt n con n el n mero de variables de la instancia del problema de satisfacci n a resolver y 2 B indica que la variable booleana x tiene un valor booleano sea
11. dos De modo pues que la motivaci n para este proyecto estriba en el hecho de que SAT fue el primer problema que se demostr que pertenece a NP Completos y que todos los problemas en esta clase son reducibles en tiempo polinomial a l Siendo as y bajo el supuesto de que estas reducciones a SAT se caractericen por polinomios de bajo grado y coeficientes peque os cual quier mejora en tiempo que se pueda realizar a los algoritmos exponenciales hoy conocidos para resolver el problema SAT es una mejora para los algorit mos exponenciales conocidos para los dem s problemas en NP completos 1 2 Breve descripci n del problema Llamaremos cl usula a la disjunci n de un conjunto finito de variables booleanas cada una de las cuales puede ocurrir con polaridad positiva no negada x o con polaridad negativa negada z7 Ejemplos de cl usulas son 21 A 2 23 21 A 23 Una f rmula es en cambio la conjunci n de un conjunto finito de cl usulas Por ejemplo F 11 V 2 V T3 A 11 V T2 A 23 es una cl usula El problema de la satisfacci n booleana SAT consiste de la forma general de las instancias al problema y de la pregunta 1 La forma general de las instancias Dados un conjunto finito de variables booleanas 11 73 T y una f rmula booleana F x1 t2 Tn en forma normal conjuntiva CNF 2 La pregunta cuya respuesta se quiere determinar existe una asignaci n de valores de verdad a las variables 21
12. implementar 2 2 Fase de selecci n de variables a asignar 2 3 Fase de deducci n Una vez que se ha seleccionado una variable para asignar junto al valor que se le asignar se inicia la fase de deducci n del algoritmo DPLL Es en esta fase que se procede a la identificaci n y propagaci n de cl usulas unitarias En esta secci n describiremos los algoritmos de propagaci n de restricciones booleanas y de identificaci n y eliminaci n de literales puros 2 3 1 Identificaci n y propagaci n de cl usulas unitarias Tal como se indica en 4 y con el estudio de implementaciones del algoritmo DPLL que se han realizado con el pasar de los a os sugiere que la propagaci n de cl usulas unitarias como mecanismo de deducci n parece ser el m s eficiente que se ha encontrado hasta ahora La propagaci n de cl usulas unitarias consiste en ubicar c ales cl usulas de la f rmula dada sta en forma normal conjuntiva est n compuestas de un s lo literal Estas cl usulas son llamadas cl usulas unitarias y se satis facen con asignar a ste nico literal el valor de verdad correspondiente Lo explicamos con un ejemplo En la f rmula F x1 V 2 VT3 A 1 VZ2 A Z3 la nica cl usula unitaria es 73 Si se asigna 123 0 queda la nueva f rmula Fs 11 V 2 V T3 A z V T2 y bajo el supuesto de que 13 0 se tiene que F es satisfactible si y s lo si F lo es Para la implementaci n de este mecanismo de deducci
13. k lt n tal que la asignaci n de cualquier otra variable no logra satisfacer la f rmula Presentamos entonces el tipo decision level data typedef struct decision level dataf variable assigned _literal int missing_ branch list propagated_var decision level data que a continuaci n describimos 1 El campo assigned literal contiene el valor y el nombre del literal asignado en un determinado nivel de decisi n Expresado de otra forma si za B za B x B k lt n vg B es un nodo de la arborescencia recorrida con el backtracking en el momento en que se consideran una nueva variable x con un valor booleano se ha creado un nuevo nivel de decisi n caracterizado por un elemento del tipo decision_level_data en el programa Este elemento tendr en su campo assigned literal a la variable x7 con su valor 2 El campo missing branch es un valor booleano que es cierto si y s lo si se ha explorado la asignaci n de assigned literal con un s lo valor de verdad Es decir si x B za B t Ukl k lt n vk E B es un nodo de la arborescencia recorrida con el backtracking en la que la variable x fue la ltima variable asignada con un valor booleano determinado missing branch ser cierto si y s lo si el conjunto de asignaciones x B x B 2 Ugl k lt n todav a no ha sido estudiado si es nodo o no k
14. rias con 2 testigos por cl usula 4 y los llama 2 watched literals empleada por zChaff asocia a cada literal x i 1 n un par de listas la primera de ellas tiene como elementos a todas las cl usulas en las que la el literal z ocurre no negado polaridad positiva como testigo o watched literal La segunda lista asociada a x tiene como elementos a todas las cl usulas en las que el literal 7 ocurre como testigo o watched literal El programa que proponemos est orientado por los cambios que se efect an durante la ejecuci n sobre una variable global de nombre sat_st que es la nica con el tipo SAT_status en todo el programa Este tipo de dato registra 1 La informaci n que es necesario preservar de la instancia del problema de satisfacci n que se ha le do y que se pretende resolver 2 El estatus de resoluci n de un problema de satisfacci n en cualquier momento dado Por esta raz n podr amos afirmar que este es el tipo de dato m s importante de todo el programa Presentamos ahora la definici n del tipo SAT_status typedef struct SAT _status int num_vars int num clauses clause formula list pos_watched list list neg_watched _list stack backtracking_status int model SAT status para comentar sus campos con detalle Elatributo formula representa la f rmula en forma normal conjuntiva Se trata de un arreglo de cl usulas cada una de tipo clause En la implementaci n que aqu
Download Pdf Manuals
Related Search
informaci informacion del sistema informacion de mi pc informacion que cura informacion exogena dian informacion fiscal sat informacion nutricional informacion del sistema windows informacion adicional informacion de sistema respiratorio informacion en espanol informacionno obslujvane informacion confidencial informacion de este equipo informacion per mjedisin informacion per skenderbeun informacion de contacto informacion personal en ingles informacion de honduras informacion de la computadora informacije o sistemu informacion del estudiante informacion de mexico informacion exogena informacion de caso informacion de excel