Beyond the Structure of SAT Formulas

Résumé

Hoy en día, muchos problemas del mundo real son codificados en instancias SAT y resueltos eficientemente por modernos SAT solvers. Estos solvers, usualmente conocidos como Conflict-Driven Clause Learning (CDCL: Aprendizaje de cláusulas guiado por conflictos) SAT solvers, incluyen una variedad de sofisticadas técnicas, como el aprendizaje de cláusulas, estructuras de datos perezosas, heurísticas de ramificación adaptativas basadas en los conflictos, o reinicios aleatorios, entre otros. Sin embargo, las razones de su eficiencia resolviendo problemas SAT del mundo real, o industriales, son todavía desconocidas. La creencia común en la comunidad SAT es que estas técnicas explotan alguna estructura oculta de los problemas del mundo real. En esta tesis, primeramente se caracteriza algunas importantes características de la estructura subyacente de las instancias SAT industriales. Específicamente, estas son la estructura de comunidades y la estructura auto-similar. Se observa que la mayoría de las fórmulas SAT industriales, vistas como grafos, tienen estas dos propiedades. Esto significa que (i) en un grafo con una estructura de comunidades clara; es decir, alta modularidad, se puede encontrar una partición de sus nodos en comunidades de tal forma que la mayoría de las aristas conectan nodos de la misma comunidad; y (ii) en un grafo con el patrón de auto-similitud; es decir, siendo fractal, su forma se mantiene después de re-escalados (agrupando conjuntos de nodos en uno). Se analiza también cómo estas estructuras están afectadas por los efectos de las técnicas CDCL durante la búsqueda. Usando los estudios estructurales previos, se proponen tres aplicaciones. Primero, se aborda el problema de la generación aleatoria de instancias SAT pseudo-industriales usando la noción de modularidad. Nuestro modelo genera instancias similares a las (clásicas) fórmulas SAT aleatorias cuando la modularidad es baja, pero cuando este valor es alto, nuestro modelo también es adecuado para modelar problemas pseudo-industriales realísticamente. Segundo, se propone un método basado en la estructura en comunidades de la instancia para detectar cláusulas aprendidas relevantes. Nuestra técnica aumenta la instancia original con un conjunto de cláusulas relevantes, y esto resulta en una mejora general de la eficiencia de varios CDCL SAT solvers. Finalmente, se analiza la clasificación de instancias SAT industrial en familias usando las características estructurales previamente analizadas, y se comparan con otros clasificadores comúnmente usados en aproximaciones SAT portfolio. En resumen, esta disertación extiende nuestro conocimiento sobre la estructura de las instancias SAT, con el objetivo de explicar mejor el éxito de las técnicas CDCL, con la posibilidad de mejorarlas; y propone una serie de aplicaciones basadas en este análisis de la estructura subyacente de las fórmulas SAT.