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, opts) Satisfy(expr, alpha, opts)

Parameters

 expr - Boolean expression alpha - (optional) list or set of names opts - (optional) zero or more options as specified below

Options

 • 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.

 Name Type Default Value Description random_var_freq numeric 0 The frequency with which the decision heuristic tries to choose a random variable random_seed numeric 91648253 Used by the random variable selection ccmin_mode nonnegint 2 Controls conflict clause minimization (0=none, 1=basic, 2=deep) phase_saving nonnegint 2 Controls the level of phase saving (0=none, 1=limited, 2=full) rnd_init_act truefalse false Randomize the initial activity luby_restart truefalse true Use the Luby restart sequence restart_first posint 100 The base restart interval restart_inc numeric 2 Restart interval increase factor garbage_frac numeric 0.20 The fraction of wasted memory allowed before a garbage collection is triggered step_size numeric 0.4 Initially use this step-size value when calculating the exponentially weighted moving averages step_size_dec numeric 1e-06 Decrement the step-size by this value after each conflict min_step_size numeric 0.06 Stop decrementing the step-size once it reaches this value

Description

 • 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.

Definitions

 • 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.

Examples

Test a simple Boolean expression for satisfiability.

 > $\mathrm{with}\left(\mathrm{Logic}\right):$
 > $\mathrm{Satisfiable}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\right)$
 ${\mathrm{true}}$ (1)

Find a satisfying assignment.

 > $\mathrm{Satisfy}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b\right)$
 $\left\{{a}{=}{\mathrm{true}}{,}{b}{=}{\mathrm{false}}\right\}$ (2)

Find a satisfying assignment while specifying the variable set to be {a,b,c}.

 > $\mathrm{Satisfy}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&or\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}b,\left\{a,b,c\right\}\right)$
 $\left\{{a}{=}{\mathrm{true}}{,}{b}{=}{\mathrm{false}}{,}{c}{=}{\mathrm{false}}\right\}$ (3)
 > $\mathrm{Satisfiable}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(¬\left(a\right)\right)\right)$
 ${\mathrm{false}}$ (4)

The following returns NULL since it is unsatisfiable.

 > $\mathrm{Satisfy}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&and\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(¬\left(a\right)\right)\right)$

Test a Boolean expression for satisfiability, while providing customized values for the step_size and rnd_init_act MapleSAT parameters.

 > $\mathrm{Satisfy}\left(a\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&implies\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(b\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}&xor\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left(¬\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\}$ (5)

References

 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.

Compatibility

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