method="maplesat" or "legacy"

The method option specifies the method which should be used for determining the solvability of the Boolean expression.  The default behavior uses the MapleSAT SAT solver but the Satisfy command also supports a method which uses a legacy Maple implementation.

solveroptions=list(equation)

By specifying a list of equations as the value of option solveroptions, it is possible to fine-tune the configuration of the MapleSAT engine. Each such equation must be of the form optionname = value. Available options are described in the following table. Each such option corresponds in name, type, and default value to a configuration option offered by MapleSAT. For more information, consult the MapleSAT and MiniSat documentation.

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.

The Satisfy command does not specify which satisfying assignment it returns. Two satisfiable formulae which are logically equivalent may produce different satisfying assignments.

If the optional second parameter to Satisfy is present, the valuation includes all variable names in alpha.

A satisfying assignment is an assignment to the variables of a given Boolean expression that satisfies the expression.

The problem of determining whether a Boolean formula has a satisfying assignment is known as the Boolean satisfiability problem or SAT. This is a decision problem which is known to be NP-complete, and consequently no polynomial-time algorithm is presently known.

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

$\mathrm{Satisfiable}\left(a\&orb\right)$

$\mathrm{true}$

$\mathrm{Satisfy}\left(a\&orb\right)$

$\left\{a=\mathrm{true}\,b=\mathrm{false}\right\}$

$\mathrm{Satisfy}\left(a\&orb\,\left\{a\,b\,c\right\}\right)$

$\left\{a=\mathrm{true}\,b=\mathrm{false}\,c=\mathrm{false}\right\}$

$\mathrm{Satisfiable}\left(a\&and\left(\&not\left(a\right)\right)\right)$

$\mathrm{false}$

$\mathrm{Satisfy}\left(a\&and\left(\&not\left(a\right)\right)\right)$

$\mathrm{Satisfy}\left(a\&implies\left(b\&xor\left(\&not\left(c\right)\right)\right)\,\mathrm{solveroptions}=\left[\mathrm{step\_size}=0.75\,\mathrm{rnd\_init\_act}=\mathrm{true}\right]\right)$

$\left\{a=\mathrm{false}\,b=\mathrm{false}\,c=\mathrm{true}\right\}$

Liang, J. H.; Ganesh, V.; Poupart, P.; and Czarnecki, K. "Learning rate based branching heuristic for SAT solvers." International Conference on Theory and Applications of Satisfiability Testing. Springer International Publishing, 2016.

Eén, N. and Sörensson, N. "An extensible SAT-solver." International Conference on Theory and Applications of Satisfiability Testing. Springer, Berlin, Heidelberg, 2003.

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

For more information on Maple 2016 changes, see Updates in Maple 2016.

The Logic[Satisfy] and Logic[Satisfiable] commands were updated in Maple 2018.

The method and solveroptions options were introduced in Maple 2018.

For more information on Maple 2018 changes, see Updates in Maple 2018.