Given a Boolean formula $\mathrm{\ϕ}\left(\mathrm{x\_\_1}\,\dots \,\mathrm{x\_\_n}\right)$, the Boolean satisfiability problem asks whether there exists some choice of $\mathrm{true}$ and $\mathrm{false}$ values for $\mathrm{x\_\_1}\dots \,\mathrm{x\_\_n}$ such that $\mathrm{\varphi }\left(\mathrm{x\_\_1}\,\dots \,\mathrm{x\_\_n}\right)\=\mathrm{true}$.  This choice of variables is called a satisfying assignment, and the formula is said to be satisfiable. The satisfiability problem is known to be computationally difficult and was one of the first problems shown to be NP-complete.

Maple 2016 introduces new efficient heuristics for determining satisfiability and testing equivalence of Boolean expressions.

$\mathrm{with}\left(\mathrm{Logic}\right)\:$

$\mathrm{Satisfiable}\left( x \mathbf{and} y \mathbf{xor} \mathbf{not} z\right)$

$\mathrm{Satisfy}\left(x \mathbf{and} y \mathbf{xor} \mathbf{not} z\right)$

$\mathrm{Satisfiable}\left(x \mathbf{and} y \mathbf{and} \mathbf{not} x\right)$

$\mathrm{formula} ≔ \mathrm{Random}\left(\left[s\,t\,u\,v\,w\,x\,y\,z\right]\,\mathrm{clauses}\=20\,\mathrm{literals}\=3\,\mathrm{form}\=\mathrm{CNF}\right)$

$\mathrm{Satisfy}\left(\mathrm{formula}\right)$

The Logic:-TruthTable command now returns a DataFrame with the truth assignments for a given formula.

$\mathrm{TruthTable}\left(x \mathbf{and} y \mathbf{xor} \mathbf{not} z\right)$