Logic - Maple Programming Help

Home : Support : Online Help : Programming : Logic : Boolean : Logic Package : Logic/Satisfy

Logic

 Satisfy
 find a valuation satisfying an expression
 Satisfiable
 determine if expression can be satisfied

 Calling Sequence Satisfiable(expr) Satisfy(expr, alpha)

Parameters

 expr - Boolean expression alpha - (optional) list or set of names

Description

 • A satisfying assignment is an assignment to the variables of a given Boolean expression that satisfies the expression. If expr is not satisfiable, then NULL is returned.
 • The Satisfiable command returns true if the Boolean expression expr is satisfiable, that is, if a satisfying assignment exists. Otherwise false is returned.
 • The Satisfy command returns a set of equations representing a satisfying assignment to expr. If expr is not satisfiable, then NULL is returned.
 • If the optional second parameter to Satisfy is present, the valuation includes all variable names in alpha.

Examples

 > $\mathrm{with}\left(\mathrm{Logic}\right):$
 > $\mathrm{Satisfiable}\left(a&orb\right)$
 ${\mathrm{true}}$ (1)
 > $\mathrm{Satisfy}\left(a&orb\right)$
 $\left\{{a}{=}{\mathrm{true}}{,}{b}{=}{\mathrm{false}}\right\}$ (2)
 > $\mathrm{Satisfy}\left(a&orb,\left\{a,b,c\right\}\right)$
 $\left\{{a}{=}{\mathrm{true}}{,}{b}{=}{\mathrm{false}}{,}{c}{=}{\mathrm{false}}\right\}$ (3)
 > $\mathrm{Satisfiable}\left(a&and\mathrm{¬}\left(a\right)\right)$
 ${\mathrm{false}}$ (4)

The following returns NULL since it is unsatisfiable.

 > $\mathrm{Satisfy}\left(a&and\mathrm{¬}\left(a\right)\right)$
 > $\mathrm{Satisfy}\left(a&impliesb&xor\mathrm{¬}\left(c\right)\right)$
 $\left\{{a}{=}{\mathrm{false}}{,}{b}{=}{\mathrm{true}}{,}{c}{=}{\mathrm{false}}\right\}$ (5)

Compatibility

 • The Logic[Satisfiable] command was introduced in Maple 2016.
 • The Logic[Satisfy] command was updated in Maple 2016.