PDF de programación - Demostración automática en paralelo en ambientes MPI, de memoria compartida y de tipo heterogéneo

CENTRO DE INVESTIGACI ÓN Y DE ESTUDIOS AVANZADOS

DEL INSTITUTO POLIT ÉCNICO NACIONAL

Unidad Zacatenco

Departamento de Computación

Demostración automática en paralelo en ambientes
MPI, de memoria compartida y de tipo heterogéneo

Tesis que presenta

Renato Zacapala Zacapala

para obtener el Grado de
Maestro en Ciencias
en la Especialidad de
Ingeniería Eléctrica

Opción

Computación

Director de la Tesis: Dr. Guillermo Morales Luna

México, D.F.

Mayo 2007

A mis padres; y a todos cuantos
hicieron posible éste momento.

Agradecimientos

Al Consejo Nacional de Ciencia y Tecnología por la beca otorgada, subven-

ción necesaria para la realización de este posgrado.

A la Biblioteca de Ingeniería Eléctrica por haber proporcionado sus materiales

de consulta durante el transcurso de la maestría.

A mi asesor el Dr. Guillermo Morales Luna, por dedicarme un poco de su pre-
ciado tiempo, tiempo durante el cual me orientó y brindo parte de su conocimiento
que a la larga hicieron posible la finalización de esta tesis.

Quiero dar gracias también al Dr. José Oscar Olmedo Aguirre y al Dr. Sergio
Víctor Chapa Vergara por sus valiosos comentarios durante la revisión del docu-
mento de tesis.

A Sofía Reza Cruz por su apoyo en la realización de todos aquellos trámi-
tes administrativos que se realizaron durante mi estancia, pero sobre todo por la
actitud que siempre tuvo con todos nosotros.

Al personal de la Biblioteca de Ingeniería Eléctrica por su ayuda para encon-

trar aquellos libros y artículos que componen parte de este documento

Y finalmente, pero no por eso menos importante, a todos los amigos que tuve

la fortuna de conocer y que hicieron más amena la estadía en el Centro.

V

Resumen

La demostración automática de teoremas consiste de métodos algorítmicos
para lograr demostraciones por medio de una computadora. La dificultad para re-
solver un problema puede depender del tipo de lógica que se utilice, en nuestro ca-
so, al utilizar la Lógica Proposicional el problema es decidible pero NP-completo.
Por lo que para resolverlos solo existen algoritmos directos de tiempo exponen-
cial en el peor caso. De ahí la importancia de disminuir el tiempo de ejecución de
cualquier implementación.

La satisfactibilidad proposicional (SAT) es un problema importante en las
ciencias de la computación debido a que la mayoría de las veces es más eficiente
pasar un problema a SAT y resolverlo con alguno de los programas existentes,
que desarrollar una versión particular para dicho problema. Recientemente ha si-
do muy importante para una amplia gama de aplicaciones practicas las cuales
incluyen el diseño, síntesis y verificación de circuitos integrados, optimización de
FPGA, inteligencia artificial y planificación de tareas. Una de las principales apli-
caciones que han motivado un nuevo auge de los resolvedores de satisfactibilidad
ha sido la verificación de circuitos integrados, dando como resultado un desarrollo
acelerado de nuevos diseños.

En este trabajo presentamos diversas implementaciones del algoritmo de Davis-
Putnam, que permiten la experimentación con el algoritmo por medio de la modifi-
cación de las variables que influyen directamente en su desempeño. Las versiones
paralelas se desarrollaron con pThreads y MPI, con el fin de obtener una eficiencia
mejor que la versión secuencial al valernos de la utilización de varios procesado-
res. Con las implementaciones en paralelo se experimentaron diversas estrategias
de selección de cláusulas y literales para hacer más eficiente el algoritmo.

VII

Abstract

The automatic demonstration of theorems consists of algorithmic methods to
construct or to localize demonstrations. The difficulty to solve a problem can de-
pend on the kind of logic that is utilized. In our case, when the problem use Logic
Propositional, it is decidible but NP-complete. There are direct algorithms but
they solve the SAT problem on exponential time. So we can see the importance to
decrease the run time of any implementation.

The propositional satisfiability ( SAT ) is an important problem in computer
sciences because most of the time it is more efficient to solve the problem with a
SAT solver, that to develop a particular version for the aforementioned problem.
The propositional satisfiability problem has been very important for an ample ran-
ge of practical applications which include the design, synthesis and verification
of chips, FPGA’s optimization, artificial intelligence and planning of tasks. One
of the principal applications that have motivated a new prosperity of SAT solvers
has been the verification of chips, giving as a result a rapid development of new
designs.

We presented a parallel version of Davis Putnam’s algorithm, in order to have
an algorithm with more efficiency than the sequential version. We develop several
strategies of selection of clauses and literals to do the algorithm more efficient.

IX

Índice general

Agradecimientos

Resumen

Abstract
Índice de figuras
Índice de cuadros
Índice de algoritmos

Lista de abreviaturas

Preámbulo

1. Introducción

.

.
.

1.1. Conceptos preliminares .
1.2. El problema SAT .
.

.
.
1.2.1. Variaciones de SAT .
1.2.2. Descripción general
.

.
.
.
.
.
Importancia de las aplicaciones .

1.3. Situación actual .
1.4.

.
.
.
.
.

.

.

.

.

.

.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

2. Algoritmo de Davis-Putnam
.

2.1. Algoritmo secuencial

.
.
2.1.1. Reglas de reducción .
.
2.1.2. Procedimiento general del algoritmo .
.

2.2. Algoritmo paralelo .

.
.

.
.

.
.

.
.

.
.

.
.

.
.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

XI

V

VII

IX

XVI

XVII

XIX

XXI

XXIII

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

.
.
.
.
.
.

.
.
.
.

1
2
4
6
8
9
10

13
15
19
21
24

XII

ÍNDICE GENERAL

2.2.1. Elementos de paralelización .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

3. Tratamiento computacional

.
.

.
.

.
.

.
.

.
.

.
.

.
.

.
.

3.1. Análisis de las instancias .
.
3.2. Preprocesamiento . . . .

.
.
.
.
3.2.1. Ordenamiento estático de variables
.
3.2.2. Ordenamiento dinámico de variables .
.
.
.
.
.
.

.
.
.
.
3.3. Versión secuencial
.
.
.
3.4. Versión utilizando hilos .
.
.
.
3.5. Versión con MPI
.
.
.
. . . .
3.6. Estrategias de solución .
.
.
.
3.7. División del árbol de búsqueda .
.
.
3.8. Métodos de selección de variables .
.
3.9. Paralelización por búsqueda en orden de variables predefinidas .

. . . .
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.

.
.
.
.

.
.
.
.

4. Características del sistema

.
.

.
.
.

.
.
.

.
.
.

.
.
.

4.1.1. Formato CNF . .

4.1. Representación de la entrada .
.
.

.
4.2. Uso del sistema . . . . . .

.
.
.
4.2.1. Modulo de selección de variables
.
.
.
.
.

.
.
4.3.1. Representación matricial .
.
4.3.2. Representación por cláusulas .
4.3.3. Representación por literales
.
.
.

4.4. Otras representaciones

4.3. Estructura de datos

. . .

.
.

.

.

.

.

.

.

.

.

.

.

.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

5. Resultados

5.1. Resultados de la versión secuencial .
.
5.2. Resultados de la versión de hilos .
.
.
5.3. Resultados de la versión de MPI
.
.
.
5.4. Análisis de resultados . . .
.
.
.
.
.
5.5. Comparación con otras implementaciones .

.
.
.
.

.
.
.
.

.
.
.
.

.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.

.
.
.
.
.

6. Conclusiones y trabajo futuro
6.1. Trabajo futuro . . . . . .

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

27

31
33
36
36
37
39
39
40
41
42
43
43

49
49
49
51
51
53
53
54
55
57

59
60
61
63
64
65

69
70

ÍNDICE GENERAL

A. Uso del sistema

A.1. Secuencial . . . .
A.2. Hilos . . . . . . .
A.3. MPI
. . . . . . .

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

.
.
.

Bibliografía

XIII

71
71
72
73

78

Índice de figuras

2.1. Diagrama de actividades del algoritmo secuencial recursivo .
2.2. Diagrama de actividades del algoritmo secuencial iterativo .
2.3. Reducción de la instancia .
.
.
2.4. Aplicación de las reglas de reducción .
.
2.5. Paralelización 1 .
.
.
2.6. Paralelización 2 .
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.

.
.

.
.

.
.

.
.

.
.

.
.

.
.

.
.

.
.

.
.

.

.

.

.

.

.

.
.
.
.
.
.

.
.
.
.
.
.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.
.

.
.

bilidad . . . . . .

de recursiones del algoritmo .

3.1. Relación entre cláusulas y variables, y el porcentaje de satisfacti-
.
3.2. Proporción entre cláusulas y variables y su relación con el número
.
.
.
.
.
.
.
.
.
.

.
.
.
3.3. Ordenamiento estático de variables .
.
.
3.4. Ordenamiento por modificación de MOMS.
.
.
3.5.
.
3.6. Ordenamiento dinámico de variables .
.
.
3.7. Esquema de asignación de tareas .
.
.
.
.
3.8. Esquema de paralelización .
.
.
.
.
.
3.9. Métodos de selección de variables .
.
.
.
.
3.10. Llamadas recursivas .
.
.
.
.
.
.
.
.
3.11. Llamadas recursivas 2 .

Árbol de búsqueda

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.