Boolean Satisfiability (SAT)
Finds a mapping from variable names to boolean values such that the expression evaluates to true, or proves that the expression is always false.
While boolean SAT is known to be NP-hard, this algorithm uses the DPLL/CDCL approach and can find an answer quickly even on some very large problem sizes. Additionally, this algorithm has been enhanced in two ways over traditional DPLL/CDCL solvers: it is parallelized and it can break some simple kinds of symmetries.
exp ::= true
| not <exp>
| <exp> <op> <exp>
op ::= iff | implies | xor | or | and
var ::= any word except true, false, not, iff, implies, xor, or, and
not, and, or, xor, implies, iff
Expressions are mostly whitespace-agnostic (although you will need whitespace to separate some tokens; for instance, whitespace is needed between the "not" and the "a" in the expression "not a").
The output is simply a satisfying assignment (a complete map from variable names to values) or null to indicate that no such assignment exists. Future versions of this algorithm may feature a different output format to indicate timeouts, memory shortage problems, or other practical concerns.