Resumen de Máquinas de Boltzmann para la resolución del problema de la satisfacibilidad

Alicia Emilia D'Anjou D'Anjou , Manuel Graña Romay , Francisco Javier Torrealdea Folgado , María del Carmen Hernández Gómez

• español

  Planteado el problema MAX-SAT como un problema de optimización, se estudia el diseño de una Máquina de Boltzmann (MB_E) para verificar la satisfacibilidad (SAT) de una expresión E del cálculo proposicional. Se especifica la estructura de las unidades y conexiones de la MB_E y se determinan las fuerzas de las conexiones para asegurar su comportamiento correcto. Los resultados experimentales, mediante simulación secuencial, muestran un comportamiento lineal con el número de proposiciones e insensibilidad respecto al tamaño y número de cláusulas.

• English

  Once stated the MAX-SAT problem as an optimization problem, we study the desing of a class of Boltzmann Machines (MB_E) able to verify the satisfiability (SAT) of an arbitrary propositional expression E. The structure of units and connections of the MB_E is specified, and the strengths associated with the connections are determined in order to guarantee the desired behavior. Experimental results, gathered through sequential simulation, show a linear behavior against the number of propositions involved, and the insensitivity relative to the size and number of clauses.