Simulated Annealing Artificial Neural Networks for the Satisfiability (SAT) Problem

  • T. Tambouratzis
Conference paper


A simulated annealing artificial neural network, which is based on the principles of Harmony Theory [1], 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 [1] 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.


Simulated Annealing Product Term Conjunctive Normal Form Logical Variable Logical Expression 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    Mano, M., (1984). “Digital Design”. Prentice-Hall, Inc. Englewood Cliffs, New Jersey.Google Scholar
  3. 3.
    Davis, M., Putnam, H., (1960). A Computing Procedure For Quantification Theory, Journal of the Association for Computing Machinery 7, pp. 201–215.MathSciNetMATHCrossRefGoogle Scholar
  4. 4.
    Dowling, W.F., Gallier, J.H., (1984). Linear-Time Algorithms For Testing The Satisfiability Of Propositional Horn Formulae, Journal of Logic Programming 3, pp. 267–284.MathSciNetCrossRefGoogle Scholar
  5. 5.
    Purdom, P.W., (1984). Solving Satisfiability With Less Searching, IEEE Transactions on Pattern Analysis and Machine Intelligence 6, pp. 510–513.MATHCrossRefGoogle Scholar
  6. 6.
    Monier, B., Speckenmeyer, E., (1985). Solving Satisfiability In Less Than 2 n Steps, Discrete Applied Mathematics 10, pp. 287–295.MathSciNetCrossRefGoogle Scholar
  7. 7.
    Gallo, G., Urbani, G., (1989). Algorithms For Testing The Satisfiability Of Propositional Formulae, Journal of Logic Programming 7, pp. 45–61.MathSciNetMATHCrossRefGoogle Scholar
  8. 8.
    van Gelder, A., (1988). A Satisfiability Tester For Nonclausal Propositional Calculus, Information and Computation 44, pp. 1–21.CrossRefGoogle Scholar
  9. 9.
    Hansen, P., Jaumard, B., (1990). Algorithms For The Maximum Satisfiability Problem, Computing 44, pp. 279–303.MathSciNetMATHCrossRefGoogle Scholar
  10. 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
  11. 11.
    d’Anjou, A., Grana, M., Torrealdea, F.J., Hernandez, M.C. (1993). Solving Satisfiability Via Boltzmann Machines, IEEE Transaction on Pattern Analysis and Machine Intelligence 15, pp. 514–521.CrossRefGoogle Scholar
  12. 12.
    Gu, J, (1993). Local Search For Satisfiability (SAT) Problem, IEEE Transactions on Systems Man and Cybernetics 23, pp. 1108–1129.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag/Wien 1995

Authors and Affiliations

  • T. Tambouratzis
    • 1
  1. 1.Institute of Informatics & TelecommunicationsNRCPS “Demokritos”Aghia ParaskeviGreece

Personalised recommendations