%0 Thesis
%A Hernández Cerezo, Alejandro
%T Estrategias para la implementación de algoritmos de satisfactibilidad en lógica de reescritura
%D 2020
%U https://hdl.handle.net/20.500.14352/254
%X El problema de satisfactibilidad booleana (SAT) consiste en determinar si existe o no una asignación válida de variables que satisfaga un conjunto de fórmulas lógicas. Este problema es un problema clásico de las ciencias de la computación, siendo el primer problema catalogado como NP-completo. Además, tiene multitud de aplicaciones tanto en otros campos de estudio como a nivel industrial.La mayoría de resolutores SAT actuales se basan en el cálculo de David-Putnam-Logemann-Loveland (DPLL), un sistema de reglas completo que certifica poder encontrar una asignación válida en el caso de que exista. Existen otros cálculos más avanzados, como el cálculo de Tinelli, que modelan algunas de las técnicas avanzadas que se utilizan en los resolutores actuales: backjump, aprendizaje de cláusulas o reinicios selectivos. Otras técnicas consisten en aplicar de manera razonada las reglas de inferencia conforme a ciertas heurísticas, por lo que se necesita una separación clara entre el sistema de reglas y las heurísticas.La lógica de reescritura es un marco ideal para estudiar estas técnicas. En ella, se hace una separación explícita en 3 niveles: ecuaciones, en donde podemos definir las operaciones y predicados auxiliares; reglas, en el que se incluyen las reglas de inferencia; y estrategias, donde controlamos la aplicación de reglas conforme a estas heurísticas.El objetivo de este trabajo es adaptar las reglas del cálculo de Tinelli al sistema Maude, refinando y extendiendo algunas de sus declaraciones. Se incluirán las técnicas de resolutores SAT actuales mencionadas anteriormente, así como una comparación de distintas heurísticas definidas en algunos de los resolutores más famosos. Para ello, estudiaremos en detalle y utilizaremos el lenguaje de estrategias de Maude, una funcionalidad menos conocida de este sistema que permite aplicar las reglas de una forma controlada y eficiente. Además, se realizarán distintos experimentos comparando la eficiencia de distintas estrategias
%X The Boolean satisfiability problem (SAT) consists of determining whether there exists an assignment that satisfies a given Boolean formula. SAT is a classic computer science problem, as it was the first problem proven to be NP-complete. SAT has also many applications in different fields.Most modern SAT solvers are based on the David-Putnam Logemann-Loveland algorithm (DPLL), a complete backtracking-based search algorithm that manages to find a valid assignment in case it exists.Tinelli’s inference system extends this version to include other modern features, such as backjump, clause learning and restarts. Modern SAT solvers also include heuristics, so we are interested in studying both rules and heuristics to understand how they work. There is usually no clear separation between these two levels, making it difficult to understand both aspects.Rewriting logic is an interesting framework to study these techniques. Declarations can be included in three different levels: equations, rules and strategies. The equation level includes declarations of logical symbols and auxiliary predicates which are needed to declare the rules in the inference system. These rules are declared in the rule level. The strategy level contains statements to control how rules are applied, so heuristics are represented in this level.The goal of this work is to study different modern SAT solvers’ techniques by adapting them to rewriting logic. For this purpose, we will implement Tinelli’s framework into the Maude system, extending its declarations to include other techniques. Therefore, we will study in detail how these techniques and heuristics work, and how to implement them in Maude. This project also aims to show the capabilities of the strategy language, which is a functionality recently released in Maude for controlling the application of rules. Furthermore, we will perform experiments to compare the performance of these techniques.
%~