SAT solving via Algebraic Normal Form and GPU

Ballesteros González, Ignacio (2021). SAT solving via Algebraic Normal Form and GPU. Thesis (Master thesis), E.T.S. de Ingenieros Informáticos (UPM).

Description

Title: SAT solving via Algebraic Normal Form and GPU
Author/s:
  • Ballesteros González, Ignacio
Contributor/s:
  • Mariño Carballo, Julio
Item Type: Thesis (Master thesis)
Masters title: Métodos Formales en Ingeniería Informática
Date: 16 July 2021
Subjects:
Faculty: E.T.S. de Ingenieros Informáticos (UPM)
Department: Lenguajes y Sistemas Informáticos e Ingeniería del Software
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (455kB) | Preview

Abstract

El problema de satisfacibilidad booleana (SAT) fue el primer problema en demostrarse NP-Completo. Muchos problemas complejos se resuelven reduciéndolos primero a problemas SAT, así que sus aplicaciones pueden alcanzar varias disciplinas. Todo problema que se pueda expresar mediante restricciones puede ser resuelto por SAT, como por ejemplo la verificación de circuitos o de software. Cualquier algoritmo aplicado a SAT que resulte ser eficiente tiene un profundo potencial de impacto en cualquiera de sus aplicaciones. Es por esto que los SAT solvers se han ido mejorando de manera constante, con la capacidad de abordar modelos cada vez más complejos inimaginables de resolver hace solo unas décadas. Los SAT solvers se basan generalmente en algoritmos de backtracking a los que se les ha añadido análisis de conflictos para recorrer de una forma más eficiente el espacio de búsqueda. Todo esto sumado al desarrollo de estructuras de datos eficientes y al diseño de heurísticas avanzadas han logrado posicionar a los SAT solvers como herramientas muy competitivas. El avance en nuevas arquitecturas también ha tenido un rol importante en la evolución de los SAT solvers. La especialización de los algoritmos paralelos y distribuidos para SAT ha abierto nuevas ramas donde estos solvers pueden competir. Aquellos que se han basado en la aceleración por hardware han creado oportunidades para lograr algoritmos más potentes y eficientes, pero de la mano han traído los desafíos de adaptar unos algoritmos que no necesariamente encajan en estos componentes como las GPU. En este trabajo presentamos el estudio de un algoritmo para resolver SAT en un entorno altamente paralelo como la GPU. Los SAT solvers suelen partir de una representación de las fórmulas booleanas en forma normal conjuntiva (CNF). Esta representación tiene unas propiedades que se aprovechan satisfactoriamente en los algoritmos de backtracking, habitualmente diseñados para la ejecución secuencial. Sin embargo, existen otras representaciones de las fórmulas booleanas con propiedades que pueden encajar mejor en un contexto paralelo. La forma normal algebraica (ANF) es una de estas representaciones que posee una operación altamente paralelizable que podría realizarse en una GPU. Las formulas ANF, también conocidas como polinomios de Zhegalkin, es una representación algebraica booleana en forma de polinomio de números enteros modulo dos (Z2). En este trabajo hemos desarrollado una herramienta que aplica un preprocesado a fórmulas en CNF y proposicionales para convertirlas en un conjunto de restricciones en ANF. Mediante ellas, podemos comprobar las satisfacibilidad de un problema encontrando el polinomio 0, el único que no es satisfacible con la representación ANF. El proceso se realiza mediante dos pasos: 1.- Multiplicación de dos polinomios y 2.- La reducción del polinomio resultante a una forma ANF canónica. Estos polinomios tienden a crecer exponencialmente cuando se les aplican las nuevas restricciones. Para acelerar la ejecución de estos dos pasos hemos desarrollado un algoritmo paralelo que aprovecha los beneficios de componentes como la GPU. Este estudio mejora el desarrollo de un solver previo basado en esta misma técnica, superando algunos desafíos que se presentaron en ese caso y con resultado prometedores en su potencial de paralelización. Como desarrollo futuro, se podría tratar de integrar esta herramienta en alguno de los SAT solvers ya existentes.---ABSTRACT---Boolean Satisfiability Problem (SAT) is the first problem in Computer Science to have been proven NP-Complete. We can encode complex problems as SAT, and its applications are spread across many fields. The application of SAT reaches anything that we can express as a problem of constraints, from circuit verification to bounded model checking. Any efficient algorithm applied to solving SAT can have a deep impact in all of its applications, so SAT solvers have been steadily improving, supporting complex models that were unimaginable to solve a couple of decades ago. These SAT solvers have been mainly based on backtracking algorithms, including conflict clause analysis to efficiently traverse the search space. The implementation of efficient data structures and clever heuristics made possible the development of competitive SAT solvers. Computer architecture has played a major role in the evolution of SAT solvers. The specialization of parallel and distributed algorithms for SAT solving has open new competition branches for solvers. Hardware-accelerated solvers open new opportunities for efficient implementations, but the challenges that arise in these architectures, like GPUs, are difficult to fit in the traditional algorithms. In this work we study a case of SAT solving in GPU. SAT solvers commonly digest a boolean formula in Conjunctive normal form (CNF). This encoding has great properties when used in backtracking solvers, which are commonly designed as sequential algorithms. However, there are other boolean formula representations with better properties for parallel algorithms. Algebraic normal form (ANF) offers an exploitable parallel operation that can be efficiently done in GPU. ANF, also known as Zhegalkin polynomial, is an algebra representing boolean formulas as a polynomial over Z2. We have developed a tool that pre-processes CNF and propositional formulas, converting them to a set of ANF constraints. We check satisfiability by finding the 0 polynomial, the only ANF representation that is unsatisfiable. This process is done as an iteration of two steps: 1.- Multiply two polynomials and, 2.- Reduce the resulting polynomial to canonical ANF. These polynomials tends to grow exponentially in size as we multiply them with new constraints. We have developed parallel algorithms that take advantages of the GPU architecture and speed up both stages. This study improves the development of a previous solver based on this technique, overcoming challenges in the implementation of these methods and with promising parallelization results. Further development could be done to apply this tool as a component of existing SAT solvers.

More information

Item ID: 68721
DC Identifier: https://oa.upm.es/68721/
OAI Identifier: oai:oa.upm.es:68721
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 08 Oct 2021 14:02
Last Modified: 08 Oct 2021 14:02
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM