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

El satisfi? Problema capacidad (SAT) es un clásico problema NP-completo de aplicación útil en muchas áreas de la informática, la ingeniería eléctrica y matemáticas. En este trabajo se presenta una integración de todos los componentes del sistema de DPLL mejorado con Redes Neuronales (NN DPLL) con el fin de crear un entorno de ejecución de usuario amigable. Uno de los principales componentes de DPLL NN es un algoritmo que es capaz de resolver algunos casos el problema de 3SAT, un conocido problema NP-completo derivado de SAT. DPLL NN combina las reglas Davis-Putnam con redes neuronales, que son lo suficientemente capaces de aprender problemas complejos. El entorno propuesto permite al usuario determinar el satisfi? Capacidad de una fórmula particular, ya sea aleatoriamente o generado manualmente. Además, el entorno proporciona una representación gráfica de árbol de los valores de asignación correspondientes que satisfacen la fórmula (si puede ser satisfi? Ed).