You can select and try out several solver algorithms: the "DPLL better" is the best solver amongst the options. Read from here about the differences between algorithms.

One single suitable set of values is enough as a solution: the solver algorithms stop and do not try to find additional solutions. Some of the solver algorithms output the suitable values, but some do not, or output a partial set.

It may also happen that the formula is false for all possible values of variables: if so, the solver algorithms report that after exhausting the search options. For example, (a -> b) & a & -b is always false.

Notice that you can check whether some formula F is always true by trying to solve the negated formula -F: in case -F is always false, F must be always true.

The algorithms may optionally output a trace of the search process. Select "html trace" to see the search process: again, read from here about the search methods used by the algorithms.

For formula-syntax input the solvers first convert the formula to a clause normal form: for certain kinds of formulas this conversion step may create a huge output, but in most cases it is a sensible simplification before actual search.

• The truth table prints a full truth table of a formula up to 1024 rows: nice for checking out small propositional formulas.

• The clause normal form is a conjunctive normal form just as used by the solvers. The conversion algorithm used is very simple and does not perform any optimizations. In many cases the optimized converters like the Tseitin transformation would give a much smaller output much faster.

• The parse tree prints a formula as a nested list built by the simple recursive descent parser. This list is later used by the clause normal form converter to build the form suitable for solvers. Check the parse tree in case you are not sure how the system understands your formula.

The options for the type of a problem are:

• random 3-sat generates a random set of clauses of length 3, using the number of variables you choose: problems containing more variables are, on the average, harder to solve. The number of clauses is always four times the number of variables: this is, on the average, a specially hard-to-solve ratio for solvers.

  For DPLL try out 200 variables or more. Truth table solvers start running into trouble with more than 20 variables. The resolution provers are a bit better than the truth table solvers, yet much worse than the DPLL solvers.

• all combinations generates a set of clauses representing all possible combinations of the input variables: any such set is unsatisfiable (i.e. no values of variables can make it true). The number of clauses is hence always two to the power of the number of variables.
• small unsat generates a very small unsatisfiable clause set, consisting of a single long clause containing all the variables and N single-element clauses containing all variables negated.

You can also browse and read the contents of a file into the input area: essentially copy-paste from a file.