Simulated Annealing Artificial Neural Networks for the Satisfiability (SAT) Problem
A simulated annealing artificial neural network, which is based on the principles of Harmony Theory , is proposed for the solution of the satisfiability (SAT) problem of propositional calculus. The structure of the employed network is such that not only is a valid solution to any given SAT problem automatically provided, but — furthermore — this solution contains the values of the variables which render true the greatest possible number of clauses.
The number of clauses which are satisfied is automatically revealed by the quantitative measure of harmony  once the simulated annealing settling procedure has been completed. Additionally, both the identity of the satisfied clauses and the actual values of all variables are determined by the settled-upon activation values of the network nodes.
KeywordsSimulated Annealing Product Term Conjunctive Normal Form Logical Variable Logical Expression
Unable to display preview. Download preview PDF.
- 1.Smolensky, P., (1986). Information Processing In Dynamical Systems: Foundations Of Harmony Theory, pp. 194–281, in D.E Rumelhart, J.L. McClelland (eds), “Parallel Distributed Processing: Foundations (Vol 1)”. MIT Press, Cambridge.Google Scholar
- 2.Mano, M., (1984). “Digital Design”. Prentice-Hall, Inc. Englewood Cliffs, New Jersey.Google Scholar
- 10.Pinkas, G., (1990). Energy Minimisation And The Satisfiability Of Propositional Logic, in D.S. Touretzky, J.L. Elman, T.J. Sejnowski, G.E. Hinton (eds) Proceedings of the “1990 Connectionist Summer School”, San Mateo, California.Google Scholar