Logic as energy:: A SAT-Based approach

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.