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

You do not appear to have Java enabled on this browser. (Note that Java is no longer supplied by default on Windows systems). The latest Java environment can be downloaded and installed from the Java website

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.

This is an example of an NP-complete problem. It is solved here by what is known as the 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