
Calling Sequence


Satisfiable(expr,options)
Satisfy(expr,options)


Parameters


expr



set, function, or boolean; expression to be checked for satisfiability

options



(optional) options as specified below





Options



The value of option logic is a string which must correspond to one of the following logic names defined by the SMTLIB standard: "QF_UF", "QF_LIA", "QF_NIA", "QF_LRA", "QF_NRA", "LIA", and "LRA".

•

timelimit = positive or infinity


Specify a time limit for the call to the SMT solver. A nonzero value represents a time budget in seconds. The default is infinity, meaning no limit is imposed.



Description


•

The Satisfiable(expr) command checks whether the SMT problem given by the expression expr can be satisfied.

•

The Satisfy(expr) command finds a solution for the SMT problem given by the expression expr.



Details


•

The Satisfiable and Satisfy commands first transform the input expr to the SMTLIB input format using ToString, and pass the resulting SMTLIB expression to an SMT solver.

•

For details on what operators and functions are permitted in the input expression and how types are inferred and declared, see the ToString help page.

•

As all Boolean formulas are SMT expressions, the Satisfiable and Satisfy commands may be viewed as generalizations of the functionality of Logic[Satisfiable] and Logic[Satisfy] respectively.


Test for the satisfiability of this simple Boolean problem.

>

e := (a or b) and (not a or not b) and (a or not b);

${e}{\u2254}\left({a}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{\textstyle {\mathbf{or}}}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{b}\right)\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{\textstyle {\mathbf{and}}}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{\textstyle {\mathbf{not}}}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}\left({a}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{\textstyle {\mathbf{and}}}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{b}\right)\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{\textstyle {\mathbf{and}}}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}\left({a}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{\textstyle {\mathbf{or}}}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{\textstyle {\mathbf{not}}}\phantom{\rule[0.0ex]{0.3em}{0.0ex}}{b}\right)$
 (1) 

Generate a satisfying instance for the preceding problem.

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

Find a solution for this Diophantine problem over quantifierfree integer linear arithmetic.

>

Satisfy( {x+y=3,2*x+3*y=5}, logic="QF_LIA" );

$\left\{{x}{=}{4}{\,}{y}{=}{\mathrm{1}}\right\}$
 (4) 

Find a Pythagorean triple.

>

Satisfy( x^2+y^2=z^2 ) assuming posint;

$\left\{{x}{=}{5}{\,}{y}{=}{12}{\,}{z}{=}{13}\right\}$
 (5) 

Find a bigger Pythagorean triple.

>

Satisfy( x^2+y^2=z^2 ) assuming posint,x>1000,y>1000,z>1000;

$\left\{{x}{=}{1647}{\,}{y}{=}{2196}{\,}{z}{=}{2745}\right\}$
 (6) 

Show that there are no solutions to the following problem.

>

Satisfiable( {x^2+y^2+z^2<1, x*y*z>1} ) assuming real;



Compatibility


•

The SMTLIB[Satisfiable] and SMTLIB[Satisfy] commands were introduced in Maple 2018.

•

The SMTLIB[Satisfiable] and SMTLIB[Satisfy] commands were updated in Maple 2020.

•

The timelimit option was introduced in Maple 2020.



