## Boolean Formula Satisfiability

The applet below generates a Boolean formula with 100 clauses and 26 variables, represented by A to Z. Each clause has 3 literals which are OR'ed together. Each literal is either one of the variables or its negation, which is represented by the lower case form of the letter. The task is to find settings for each of the variables which make all of the clauses true. You have the choice of either generating a random formula, which may or may not have a solution, or a formula which is guaranteed to have a solution. You can get the computer to solve the problem by pressing the*Solve*button

### Further Information

This applet is based on ideas described on the following websites: Constraint Satisfaction Problems and SAT Instance Generation . You may also be interested in SATLive. |

**DPLL**algorithm. This algorithm actually turned out to be a lot quicker than I expected (so I put in a delay at each step). This is a fairly simple example, as such problems go, and more advanced methods of solving, and generating, such Boolean formulae can be found on the websites listed

Source Code