Evolutionary SAT Solver (ESS)
Oscar Pérez Cruz, Hato Rey, Alfredo Cruz · 2011
An NP problem is a class of problem whose solution can be found if possible in non-polynomial time with a non-deterministic algorithm. The Boolean Satisfiability Problem (SAT) is a well known NP-complete decision problem that consists in deciding whether the variables of a propositional logic formula can be given a value that satisfies the formula. This research will focus on digital testing by using this problem to find the growth faults within a programmable logic array (PLA) by analyzing its Boolean equation in conjunction normal form (CNF). The first stage of this project will be the development of a SAT solver which will incorporate genetic algorithms. Several tests are performed with different values for each parameter of the genetic algorithm to determine the best way to optimize the process of finding all the possible values that satisfy a PLA Boolean equation. Also, from the SAT library, several benchmarks will be used to determine which parameters optimize the process of finding a solution to the problem. These tests will be evaluated by how many solutions are found and the amount of time it takes to find a solution to the problem within a convergence and generation limit.