Satisfiability Algorithms implemented in python
This program starts by prompting the user to enter a number for their desired algorithm to run from a choice of 3: WalkSAT, Simulated Annealing, and Genetic Algorithm. Upon choosing an algorithm the user is able to pick a directory with which they would like to pull files from to feed formulas into the program. Depending on the algorithm chosen, the program will call specific functions to solve the satisfiability problem or get the best or most satisfiable solution. For reference, each function counts the number of satisfied clauses and compares to previously obtained values to ensure the maximum is returned. After running the algorithms the program returns a graph that represents the average clauses satisfied for each formula and one that shows the CPU time for each as well.
Algorithms:
- WalkSAT - WalkSAT is a form of local search or hill climbing that works to change values in a manner than returns the maximum possible reward. The algorithm first generates a random solution to the formula given and tests its validity. If it happens to find that the value returned is a satisfiable solution, it returns the solution and ends. If the solution is not found to be satisfactory, the algorithm does one of two things: randomly chose a value within the proposed solution to flip or pick a value to flip that leads to the lowest amount of incorrect clauses. In this implementation this was found by getting the variable number that was the most present in the incorrect clauses. The reason that the WalkSAT gives a chance to pick a random value is because there is a possibility that the algorithm will eventually get stuck flipping values back and forth and not returning a value.
2. Simulated Annealing - This algorithm is another type of local search or hill climbing, but has a slightly different approach to solving the formula at hand. The algorithm also starts by generating a random solution to the given formula. After testing its satisfiability it takes a potentially incorrect solution and flips one variable. The flipping of the variable is the key difference between Simulated Annealing and WalkSAT. In this algorithm the flipped variable is chosen by random and the new solution is compared to the previous one. If the number of satisfied clauses goes up, the random one is used for the next loop. These random flips go on for a given amount of turns and if the answer isn't satisfied it does a random restart by generating a new random solution.
3. Genetic Algorithm - The Genetic Algorithm is another that originally implements a random solution to the formula given, but is much different than the hill climbing algorithms. This algorithm generates an original population of random potential solutions to be used in the future. It is given a mating percentage as well as mutation percentage to decide how the population should change over generations. In this implementation a mating of 20% and a mutation of 3% were used. After the initial population is created, 20% of the population is randomly chosen and parents are mated to create two children that are portions of both parents. The index point chosen to split the parents is also randomly chosen. After the mating, the mutations occur on 3% of population. In these mutations one random value is flipped for each person chosen. The satisfiability is then calculated for every member of the population and if a satisfiable solution is found the algorithm returns it. If one is not found 20% of the population that have the lowest satisfiability numbers are taken out of the population. After running this algorithm on large files, I found the size of the population to get too large and time taken to go up drastically. John Miller informed me he set a point in which he desired his population to not rise and lowered it if it got to that point. So I implemented a check in the population that eliminated 80% of the population if it reached a certain threshold and made sure to keep the top scoring members of the population.
Note:
The graphs for the running of the algorithms can be found in the included directory 'graphs'. There are 6 total graphs, one for the CPU time for each algorithm implemented and one for the clauses satisfied for each algorithm. The x-axis on each graph has the individual formulas for each bar. The files from first to last go from left to right in the graph.