SATyrus: a SAT-based neuro-symbolic architecture for constraint processing

This paper introduces SATyrus, a neuro-symbolic architecture oriented to optimization problem solving via mapping problems specification into sets of pseudo-Boolean constraints. SATyrus provides a logical declarative language used to specify and compile a target problem into a particular energy function representing its space state of solutions. The resulting energy function is then mapped into a higher-order Hopfield network of stochastic neurons in order to find its global minima. The application of SATyrus over three illustrative problems are given: (i) graph coloring, (ii) traveling salesperson problem (TSP), and (iii) calculus of the difference between observed and hypothesized distances of two atoms, a sub-problem of the determination of a molecular structure.