(a -> b) & a & -bor a dimacs version of the clause normal form syntax like
-1 2 1 -2which 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 0or just
-1 2 1 -2hide syntax
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.