Un ambiente integrado de ejecución para determinar la satisfacibilidad de fórmulas en forma normal conjuntiva

Abstract

El problema de satisfacibilidad (SAT), el primero en demostrarse que es NP-completo, es fundamental en muchos campos de las ciencias de la computación, la ingeniería eléctrica y matemática. En el presente trabajo se integran todas las componentes del sistema DPLL con Redes Neuronales (DPLL RN), para crear un ambiente de ejecución amigable al usuario. Una de las componentes fundamentales del sistema DPLL RN consta de un algoritmo que permite resolver algunas instancias del problema 3SAT, un conocido problema NP-completo derivado de SAT. El sistema DPLL RN combina las reglas de Davis-Putnam con redes neuronales (DPRN), las cuales tienen una gran capacidad para aprender problemas complejos. El ambiente propuesto permite al usuario determinar la satisfacibilidad o no de una fórmula en lógica proposicional, permitiéndole ingresar una fórmula cualquiera o generar una aleatoriamente y luego se refleja en un árbol el camino seguido para obtener las asignaciones que hacen verdadera a dicha fórmula si tales asignaciones existen.

The satisfiability problem (SAT) is a classical N P-complete problem of useful application in plenty of computer science areas, electric engineering, and mathematics. In this work we present an integration of all the components of the DPLL system enhanced with Neural Networks (DPLL NN) in order to create a user friendly execution environment. One of the main components of DPLL NN is an algorithm that is capable of solving some instances of the 3SAT problem, a well-known N P-complete problem derived from SAT. DPLL NN combines the Davis-Putnam rules with neural networks which are capable enough to learn complex problems. The environment proposed allows the user determine the satisfiability of a particular formula either randomly or manually generated. In addition, the environment provides a graphical tree representation of the corresponding assignation values that satisfy that formula (if it can be satisfied).