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.

Sign In

sat

Run an Example

Install & Use