Tackling the Polarity Initialization Problem in SAT Solving Using a Genetic Algorithm

The Boolean satisfiability problem holds a significant place in computer science, finding applications across various domains. This problem consists of looking for a truth assignment to a given Boolean formula that either validates it or proves its impossibility. An indispensable element influencing the efficacy of tools designed for tackling this challenge, known as sat solvers, is the choice of an appropriate initialization strategy. This strategy encompasses the assignment of initial values, or polarities, to the variables before starting the search process. A well-crafted initialization strategy has the capability to curtail the search space and minimize the number of conflicts and backtracks by ensuring that variables are assigned values that are likely to satisfy the formula from the outset. This paper introduces an innovative initialization approach founded on genetic algorithms, which are evolutionary algorithms inspired by the principles of natural selection and reproduction. Our approach executes a genetic algorithm on the given formula, persisting until it discovers a satisfying assignment or meets predetermined termination criteria. Subsequently, it furnishes the satisfying assignment in case of success; otherwise, it employs the best assignment (that satisfies the highest number of clauses) to initialize the variables’ polarities for the sat solver.