MFSAT: a SAT solver using multi-flip local search

Local search-based methods of SAT solving have received a significant attention in the last decade. All local search-based methods choose the next truth assignment by flipping the value of only one variable. Simultaneously flipping values of multiple variables on an iteration can allow a local search-based solver to take long leaps in the search space. We report on SAT solver MFSAT, which has nine local search-based procedures. One of them is similar to conventional procedures which flip the value of one variable on an iteration. Other eight procedures are capable of simultaneously flipping values of multiple variables on an iteration to generate the successor truth assignment. We call these procedures "multi-flip" procedures. We report on the empirical evaluation of the nine procedures on more than 2700 benchmark SAT problems. Our results show that multi-flip procedures solve many more problems than the uni-flip procedure. Several multi-flip procedures solve problems many times faster than the uni-flip procedure.