An artificial neural network satisfiability tester

An artificial neural network tester for the satisfiability problem of propo sitional calculus is presented. Satisfiability is treated as a constraint s atisfaction optimization problem and, contrary to most of the existing sati sfiability testers, the expressions are converted into disjunctive normal f orm before testing. The artificial neural network is based on the principle s of harmony theory. Its basic characteristics are the simulated annealing procedure and the harmony function; the latter constitutes a measure of the satisfiability of the expression under the current truth assignment to its variables. The tester is such that: (a) the satisfiability of any expressi on is determined; (b) a truth assignment to the variables of the expression is output which renders true the greatest possible number of clauses; (c) all the truth assignments which render true the maximum number of clauses c an be produced. (C) 2001 John Wiley & Sons, Inc.