Extensions of Lagrange programming neural network for satisfiability problem and its several variations

The satisfiability problem (SAT) of the propositional calculus is a well-known NP-complete problem. It requires exponential computation time as the problem size increases. We proposed a neural network, called LPPH, for the SAT. The equilibrium point of the dynamics of the LPPH exactly corresponds to the solution of the SAT, and the dynamics does not stop at any point that is not the solution of the SAT. Experimental results show the effectiveness of the LPPH for solving the SAT. In this paper we extend the dynamics of the LPPH to solve several variations of the SAT, such as, the SAT with an objective function, the SAT with a preliminary solution, and the MAX-SAT. The effectiveness of the extensions is shown by the experiments.