README.md

## 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.

### Input Language

exp ::= true

| false

| <var>

| (<exp>)

| not <exp>

| <exp> <op> <exp>

op ::= iff | implies | xor | or | and

var ::= any word except true, false, not, iff, implies, xor, or, and

**Operator precedence:**(most tightly binding first)

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").

### Output

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.