Introduction
Satisfiability Problems are one of the popular testbeds for the performance of search algorithms in the area of artificial intelligence. To solve a satisfiability problem is to find a solution to a Boolean formula in conjunctive normal form (CNF). A formula of this kind consists of M clauses. Each clause is the disjunctive combination of a few Boolean variables. Each variable is randomly selected from N Boolean variables. A solution to a formula of this kind is an assignment of truth values to each variable that makes the whole formula true. Kirkpatrick and Selman shows that randomly generated Boolean formulae with K=2 variables per clause are almost aways satisfiable when the ratio of clauses to variables is less than 1; for ratios larger than 1, the formulae are almost never satisfiable. They also find a similar threshold behavior for higher values of K. For example, when K=3 and the ratio of clauses to variables is greater than 4.3, it is very hard to find a solution to the formula or prove that it is unsatisfiable. This poject implements several algorithms to solve SAT problems and uses a graphical interface to show the phase transition property of SAT problems.

Algorithms to Solve Satisfiability Problems
In this project, four algorithms are implemented, including Selman's WalkSat algorithm which is one of the best algorithms to solve SAT problems.

Greedy Search Algorithm
This algorithm finds the flip which can reduce the number of unsatisfied clauses and then performs that flip. It continues in this way till no flip can reduce the number of unsatisfied clauses. If the number of unsatisfied clauses is zero, then a solution is found and that the formula is satisfiable. If the number of unsatisfied clauses is greater than zero, then a local minimum is encountered or the formula is not satisfiable. Usually, greedy search is stuck at a local minimum and therefore being unable to find a solution to the problem.

WalkSat Algorithm
This is the best simple algorithm to find a solution to SAT problems. The side-walk mechanism is a very good way to escape from local minimums. The algorithm runs in this way. At each step, it randomly choose to do greedy search or side walk. Greedy search is the same as above. Side walk is to randomly choose a variable in an unsatisfied clause and flip it.  If there is a solution, this algorithm can find the solution very quickly.

Stack Chain Algorithm
This algorithm processes the formula clause by clause and tries to satisfy every clause by flipping some variable in the clause if needed. If satisfying the current clause needs to unsatisfy some already-satisfied clauses, it will do it and try to satisfy those replaced clauses in the following steps.

Queue Chain Algorithm
This algorithm is similar to the Stack Chain algorithm. The only difference is to put those replaced clauses at the end of the queue instead of the top of the stack. This means that replaced clauses will be processed at later time.

Implementation
The above algorithms are implemented in Java. For details about the implementation, please refer to the source code. I would like to talk about several interesting points in the implementation.

1) The searching process is running as a thread. In this way, it is very easy to stop the thread, restart the thread, control the speed of the searching process. In addition, it makes the applet more sensitive to control commands.
2) This program doesn't use the repaint method because repaint will cause serious flicking problems. Instead, it just paints on the previous image and thus almost eliminating flicking.

Discussion
The reason why WalkSat is very efficient lies in the fact that it balances two searching forces in a very good way, namely the force to search greedily and the force to escape local minimums. Unlike simulated annealing, the force to escape local minimums in WalkSat does not fade away as time passes by. On the contrary, it always imposes enough influence on the searching process to correct the greediness of greedy search.