Logic as Energy: A SAT-Based Approach

  • Priscila M. V. Lima
  • M. Mariela M. Morveli-Espinoza
  • Felipe M. G. França
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4729)


This paper presents the implementation of ARQ-PROP II, a limited-depth propositional reasoner, via the compilation of its specification into an exact formulation using the satyrus platform. satyrus’ compiler takes as input the definition of a problem as a set of pseudo-Boolean constraints and produces, as output, the Energy function of a higher-order artificial neural network. This way, satisfiability of a formula can be associated to global optima. In the case of ARQ-PROP II, global optima is associated to Resolution-based refutation, in such a way that allows for simplified abduction and prediction to be unified with deduction. Besides experimental results on deduction with ARQ-PROP II, this work also corrects the mapping of satisfiability into Energy minima originally proposed by Gadi Pinkas.


ARQ-PROP II higher-order neural networks propositional reasoner satisfiability satyrus 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aleksander, I., Evans, R.G., Sales, N.: Towards intentional neural systems: experiments with MAGNUS. In: Proc. of the Fourth Int. Conf. on Artificial Neural Networks, pp. 122–126 (1995)Google Scholar
  2. 2.
    Barbosa, V.C, Lima, P.M.V.: On the distributed parallel simulation of Hopfield’s neural networks. Software-Practice and Experience 20(10), 967–983 (1990)CrossRefGoogle Scholar
  3. 3.
    Dixon, H.E., Ginsberg, M.L., Parkes, A.J.: Generalizing Boolean Satisfiability I: Background and Survey of Existing Work. J. of Art. Intelligence Research 21, 193–243 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Geman, S., Geman, D.: Stochastic relaxation, Gibbs distribution, and the Bayesian restoration of images. IEEE Trans. on Pattern Analysis and Machine Intelligence PAMI-6, 721–741 (1984)CrossRefGoogle Scholar
  5. 5.
    Hopfield, J.J.: Neural networks and physical systems with emergent collective computational abilities. Proc. of the Nat. Acad. of Sciences USA 79, 2554–2558 (1982)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Kirkpatrick, S., Gellat Jr., C.D., Vecchi, M.P.: Optimization via Simulated Annealing. Science 220, 671–680 (1983)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Lima, P.M.V.: Resolution-Based Inference on Artificial Neural Networks. Ph.D. Thesis, Department of Computing. Imperial College London, UK (2000)Google Scholar
  8. 8.
    Lima, P.M.V.: A Goal-Driven Neural Propositional Interpreter. International Journal of Neural Systems 11, 311–322 (2001)MathSciNetGoogle Scholar
  9. 9.
    Pinkas, G.: Logical Inference in Symmetric Neural Networks. D.Sc. Thesis, Sever Institute of Technology, Washington University, Saint Louis, USA (1992)Google Scholar
  10. 10.
    Lima, P.M.V., Pereira, G.C., Morveli-Espinoza, M.M.M., França, F.M.G.: Mapping and Combining Combinatorial Problems into Energy Landscapes via Pseudo-Boolean Constraints. In: De Gregorio, M., Di Maio, V., Frucci, M., Musio, C. (eds.) BVAI 2005. LNCS, vol. 3704, pp. 308–317. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Lima, P.M.V., Pereira, G.C., Morveli-Espinoza, M.M.M., França, F.M.G.: SATyrus: A SAT-based Neuro-Symbolic Architecture for Constraint Processing. In: Proc. of the Fifth Int. Conf. on Hybrid Intelligent Systems, pp. 137–142 (2005)Google Scholar
  12. 12.
    Lima, P.M.V., Pereira, G.C., Morveli-Espinoza, M.M.M., França, F.M.G., Lavor, C.C.: Mapping Molecular Geometry Problems into Pseudo-Boolean Constraints. In: Proc. of the Int. Work. on Genomic Databases – IWGD 2005 (2005),
  13. 13.
    Richardson, M., Domingos, P.: Markov Logic Networks. Machine Learning 62, 107–136 (2006)CrossRefGoogle Scholar
  14. 14.
    Morveli-Espinoza, M.M.M.: Compiling Problems Resolution to Energy Minimization. M.Sc. dissert. COPPE/PESC, Universidade Federal do Rio de Janeiro (2006)Google Scholar
  15. 15.
    Silva, E.F., Lima, P.M.V., Diacovo, R., França, F.M.G.: Aggregating energy scenarios using the SATyrus neuro-symbolic tool. In: Abstracts of the 19th Int. Symp. on Mathematical Programming, pp. 146–146 (2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Priscila M. V. Lima
    • 1
  • M. Mariela M. Morveli-Espinoza
    • 2
    • 3
  • Felipe M. G. França
    • 1
    • 3
  1. 1.LAM – Computer Architecture and Microelectronics Laboratory, Universidade Federal do Rio de JaneiroBrazil
  2. 2.Departament d’Informàtica, Universitat Autònoma de BarcelonaSpain
  3. 3.COPPE – Systems Engineering and Computer Science Program, Universidade Federal do Rio de JaneiroBrazil

Personalised recommendations