Evolving a Neural Net-Based Decision and Search Heuristic for DPLL SAT Solvers

Solvers for the Boolean satisfiability problem are an important base technology for many applications. The most efficient SAT solvers for industrial applications are based on the DPLL algorithm with clause learning and conflict analysis dependent decision heuristics. The solver MINISAT V1.14 was modified to use a neural-net-based decision heuristic and search strategy. The weights and biases of the multilayer feedforward neural net are generated by an evolution strategy which is trained on a sample set of SAT problems. Problems solved with the evolved solutions encounter a similar number of conflicts as the original program, but require a higher number of decisions.