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:

• negation symbols are -, ~
• conjunction symbols are &, and
• disjunction symbols are |, v, V, or
• xor symbols are +, xor
• implication symbols are ->, =>
• equivalence symbols are <->, <=>

There is no operator precedence; all operators are bound from left:
a & b v c & d v e is read as ((((a & b) v c) & d) v e)

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: "cdcl: clause learning" implements the algorithm essentially all the modern high-performance solvers are built upon and is, together with "dpll: better", the strongest option 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.

There are three main method categories for solving classical propositional formulas:

• Truth table search: generate all possible assignment combinations for all the variables in the formula and check for each assigment whether the formula is true. Since the number of combinations is two to the power of the number of variables, this becomes infeasible for formulas with a large number of variables.
  This "truth-table: naive" method can be improved by checking also partial assigments where only some variables have been assigned values: it may happen that a formula becomes false even after just a few variables have been assigned. This is implemented as the "truth table: better" method on our page.

• Resolution search: the idea of the resolution method is to use a gneralization of modus ponens to derive new clauses from the existing clauses. Clauses are derived until all combinations are exchausted or a contradiction is derived. The resolution method should be seen as a general framework: actual solvers implement wildly different strategies and optimisations.
  Our "resolution: naive" method generates clauses in all possible ways and implements no optimizations. The "resolution: better" is significantly optimized: preprocessing clauses, literals in clauses are ordered like [-3-1,2,5], ordered resolution is used (only the first literal of a clause is selected), always selecting the shortest usable clause as given, storing and simplification by unit clauses (assigned variables), forward subsumption of selected clauses and partial backward-subsumption.
  While resolution has been the basis of most state-of-art predicate logic solvers, for propositional logic it is inferior to the DPLL method described next.

• DPLL (Davis-Putnam-Logemann-Loveland) search is essentially a constraint solver based on the combination of the truth table search with (limited) resolution. For each partial assigment of values in the truth table search we (a) test whether the formula is already false (like the "truth table: better" method above) and (b) use unit clauses (single literals) to derive new unit clauses, which is essentially a limited version of resolution.
  The DPLL method should be also seen as a general framework: actual solvers implement wildly different strategies and optimisations. An excellent source for reading about various methods used by the state of the art solvers is the collection of papers by the authors of Minisat, a popular high-end solver. The most important extension to DPLL is Conflict-Driven Clause Learning (CDCL), the algorithm essentially all the modern high-performance solvers are built upon. It is implemented on our page as the "cdcl: clause learning" solver described below.
  We provide four versions of DPLL-family solvers for experimenting, from worst (and easiest to understand) to better and more complicated:
  • dpll: naive a minimal, naive implementation of dpll with no optimizations. The code is very similar to the pure table search solver.
  • dpll: old an improved old-style (before the improvements developed in nineties) DPLL. It adds the pure literal rule (used after every unit propagation step), selects literals according to weights calculated before the start of the search, organizes clauses into buckets associated with variables.
  • dpll: better implements additional widely used optimizations on top of the "dpll: old" version (see, for example, minisat papers for explanations):
    • does not use pure literal rule during search (too time-consuming)
    • learning variable weights: the last contradiction clause adds weights to the variables it contains
    • only two literals per clause are watched
  • cdcl: clause learning extends "dpll: better" to a Conflict-Driven Clause Learning (CDCL) solver: the algorithm behind essentially all the modern high-performance solvers like kissat. On top of the machinery of "dpll: better" it adds:
    • an explicit trail of assignments, storing for each variable assigned by unit propagation the clause which forced its value: this turns the recursive search of the dpll solvers into a plain loop
    • conflict analysis: whenever a clause becomes false, these stored clauses are resolved backwards into a new learned clause pinpointing a cause of the conflict (the first unique implication point method). The learned clause is added to the clause set and guarantees that the very same conflict is never met again
    • non-chronological backtracking (backjumping): the learned clause tells how many decision levels can be jumped back over at once
    • minimizing the learned clauses, and regularly throwing away the ones which look useless: without the latter the clause set would keep growing until propagation slows down to a crawl
    • variable activities in the style of VSIDS: variables taking part in the recent conflicts are preferred when the next variable to assign is chosen
    • phase saving: a variable is first tried with the value it was last assigned
    • restarts following the Luby sequence: the search is regularly started over from the beginning, keeping the learned clauses, the activities and the saved phases
    Do not expect a miracle on the problems of our random 3-sat generator, though: uniform random problems carry no structure for the learned clauses to catch, and there "cdcl: clause learning" and "dpll: better" are roughly on par, both having a long tail of unlucky problems. Clause learning wins on problems with structure - which is what the problems coming from real applications look like - and this is why the modern solvers are built on it.

The easiest way to find top level propositional solvers is to check the The international SAT Competition: you will see the competition results for various problem categories, can download competition problems, source code and descriptions of the provers.

A good alternative choice is to check out minisat: an easily extensible and hackable state of the art solver which is a basis for several other state of the art solvers. You can even run minisat in your browser, compiled from C to javascript using LLVM.

The best known modern conflict-driven clause learning solvers are kissat and cadical by Armin Biere along with their many derivatives, dominating the recent SAT competitions: their source repositories are a good place to see how a carefully engineered CDCL solver is built. Our own "cdcl: clause learning" solver is a small educational implementation of the same core algorithm: it needs a comparable number of steps, but each step is several times slower than in a carefully optimized C solver.

The three building options "truth table", "clause normal form" and a "parse tree" are simple, useful utilities implemented in proplog_parse.js and proplog_convert.js:

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

• The clause normal form implemented in proplog_convert.js 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 implemented in proplog_parse.js 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.

Generate a problem button will call generators implemented in proplog_generate.js to generate an example problem in a simple DIMACS format of a clause normal form, suitable for solvers.

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 cdcl and 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 cdcl and 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.

The clear button simply clears the input field and result.

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