Each of my algorithms take as input the clauses from the files in conjunctive normal form (CNF). To represent this, I have a 2D array with the rows being the clauses, and the indices of the rows being the variables. If a variable appears in a clause positively, it is positive, and if it appears in the clause negated it is negative within the array.
DPLL starts by evaluating the list of clauses for any unit clauses. If there is a unit clause, it is removed from the list of clauses and the literal associated with the clause is given the satisfying assignment (literal if literal, not literal if not literal). The algorithm then searches for pure literals. These are literals that appear in only one form (positively or negatively) throughout the entire formula. For every pure literal found, it and all clauses it is in are removed from the formula and given the correct satisfying assignment. The algorithm then checks for completeness. If there are no more clauses, then the formula has been satisfied, and the algorithm returns True. If there is an empty clause, i.e., a clause that cannot be satisfied, then the algorithm returns False. After this, the algorithm picks a literal at random to test values for. For my implementation, I chose the first literal in the list, because I knew it would always be there. It then recursively calls the algorithm twice, one such that the chosen literal is positive, and one such that the chosen literal is negated. The algorithm is then repeated.
WalkSAT begins by randomly assigning each literal a True or False value. It then checks for completeness- if this assignment satisfies all clauses, then return True. If all clauses are not satisfied, then the algorithm will randomly choose an unsatisfied clause. After this, 65% of the time the algorithm will find and flip the value of the literal within that randomly chosen clause that, when flipped, will satisfy the most clauses. The other 35% of the time, a random literal value is flipped. I picked these odds because I wanted it to be more likely to flip the bit that will satisfy the most clauses, but also have a good chance to flip a random bit to avoid more easily getting stuck at local minima. The algorithm then repeats the process, checking for completeness with the new assignment created by the above steps, and repeats the rest. This occurs until a solution is found, or a time out is reached. My time-out implementation is the number of literals * 3. I did this because I wanted the time out to scale with the size of the problem, but it also needed to be big enough to allow the algorithm to be able to find a solution. My implementation also allows the algorithm to restart 100 times if the time-out is reached so that it is more likely to find a solution if there is one. WalkSAT is prone to getting stuck at local minima, so allowing restarts makes a solution more likely.
The genetic algorithm is initialized by creating a list of random assignments called the population. I made the initial population size to be 200, because a large size allows for lots of randomness and different possible outcomes. The algorithm begins by the population is sorted by their fitness, which is the number of clauses that the assignments in the population satisfy. The fittest individual is kept, and the last 6 are culled, or removed from the population. The population then reproduces to create a new population that is the same size as the current population. The parents are chosen based on their fitness, with a higher fitness being more likely to be chosen as a parent. Each child is randomly assigned half of its values from the first parent and half of its values from the second. Each child then has a 4% chance of being mutated (having a random literal within its assignment be flipped). I chose this 4% number so that it is low enough that it does not severely affect the overall population, but high enough so that getting stuck at local minima is less likely. After this, each child is added to the new population, and the algorithm is restarted with the new population, which is ideally more fit than the last. The timeout for my genetic algorithm is based on if the maximum fitness has recently changed. I keep track of the overall most fit assignment, and if that does not change within 100 generations, I assume it is stuck at local minima and I decide to restart the algorithm. The algorithm can reset up to 5 times before an ultimate time-out is declared.