 Logic - Maple Help

 Logic Boolean Satisfiability

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{true}}$ (1.1)

 $\left\{{x}{=}{\mathrm{false}}{,}{y}{=}{\mathrm{false}}{,}{z}{=}{\mathrm{false}}\right\}$ (1.2)

 ${\mathrm{false}}$ (1.3)

 $\left({s}{\vee }{t}{\vee }{y}\right){\wedge }\left({s}{\vee }{u}{\vee }{w}\right){\wedge }\left({s}{\vee }{w}{\vee }{¬}{x}\right){\wedge }\left({s}{\vee }{y}{\vee }{z}\right){\wedge }\left({t}{\vee }{w}{\vee }{y}\right){\wedge }\left({t}{\vee }{¬}{u}{\vee }{¬}{w}\right){\wedge }\left({t}{\vee }{¬}{v}{\vee }{¬}{w}\right){\wedge }\left({u}{\vee }{w}{\vee }{z}\right){\wedge }\left({u}{\vee }{y}{\vee }{¬}{z}\right){\wedge }\left({v}{\vee }{y}{\vee }{¬}{u}\right){\wedge }\left({w}{\vee }{¬}{t}{\vee }{¬}{z}\right){\wedge }\left({x}{\vee }{¬}{t}{\vee }{¬}{w}\right){\wedge }\left({x}{\vee }{¬}{t}{\vee }{¬}{z}\right){\wedge }\left({z}{\vee }{¬}{t}{\vee }{¬}{v}\right){\wedge }\left({¬}{s}{\vee }{¬}{t}{\vee }{¬}{w}\right){\wedge }\left({¬}{s}{\vee }{¬}{u}{\vee }{¬}{w}\right){\wedge }\left({¬}{s}{\vee }{¬}{v}{\vee }{¬}{y}\right){\wedge }\left({¬}{t}{\vee }{¬}{u}{\vee }{¬}{z}\right){\wedge }\left({¬}{t}{\vee }{¬}{x}{\vee }{¬}{z}\right){\wedge }\left({¬}{u}{\vee }{¬}{w}{\vee }{¬}{y}\right)$ (1.4)

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

 $\left\{{s}{=}{\mathrm{false}}{,}{t}{=}{\mathrm{false}}{,}{u}{=}{\mathrm{true}}{,}{v}{=}{\mathrm{false}}{,}{w}{=}{\mathrm{false}}{,}{x}{=}{\mathrm{false}}{,}{y}{=}{\mathrm{true}}{,}{z}{=}{\mathrm{false}}\right\}$ (1.5) Truth Tables

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