logic = string

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

For an explanation of these logics, see Formats,SMTLIB.

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.

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.

The Satisfiable and Satisfy commands first transform the input expr to the SMTLIB input format using ToString, and pass the resulting SMT-LIB 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.

with(SMTLIB):

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

$e≔\left(a\mathbf{or}b\right)\mathbf{and}\mathbf{not}\left(a\mathbf{and}b\right)\mathbf{and}\left(a\mathbf{or}\mathbf{not}b\right)$

Satisfiable(e);

$\mathrm{true}$

Generate a satisfying instance for the preceding problem.

Satisfy(e);

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

Find a solution for this Diophantine problem over quantifier-free integer linear arithmetic.

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

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

Find a Pythagorean triple.

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

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

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\}$

Show that there are no solutions to the following problem.

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

$\mathrm{false}$

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

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

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

The timelimit option was introduced in Maple 2020.

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