Use either a conventional formula syntax like
(a -> b) & a & -b
or a dimacs
version of the clause normal form syntax like
-1 2
1
-2
which is a conjunction of disjunction lines with numbers standing for variables:
the last example means simply (-x1 v x2) & x1 & -x2
For conventional formula syntax:
For dimacs you may use or skip the initial comment lines starting with c, the special p line and the final 0 symbols at the end of each disjunct. We allow the trailing 0-s only at the end of a line.
I.e. you may use the full dimacs version like
c comment
p cnf 2 3
-1 2 0
1 0
-2 0
or just
-1 2
1
-2
Solving a classical propositional formula means looking for such values of variables that the formula becomes true. For example, (a -> b) & a becomes true if and only if both a and b are assigned true.
You can select and try out several solver algorithms: the "DPLL better" is the best solver amongst the options offered on our page. Read the "Methods for solving formulas" section below about the differences between algorithms. One single suitable set of values is enough as a solution: our 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. Our solvers may optionally output a trace of the search process. Select "html trace" to see the search process. For formula-syntax input our 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 options for the type of a problem are:
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.
You can also browse and read the contents of a file into the input area: essentially copy-paste from a file.
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 options for the type of a problem are:
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.
You can also browse and read the contents of a file into the input area: essentially copy-paste from a file.