SMTLIB/Satisfy - Help

SMTLIB

 Satisfiable
 check if SMT problem is satisfiable
 Satisfy
 find satisfying instance for SMT problem

 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

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

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 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}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{b}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({a}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{b}\right)\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{and}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}\left({a}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{or}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{\mathbf{not}}\phantom{\rule[-0.0ex]{0.3em}{0.0ex}}{b}\right)$ (1)
 > Satisfiable(e);
 ${\mathrm{true}}$ (2)
 Generate a satisfying instance for the preceding problem.
 > Satisfy(e);
 $\left\{{a}{=}{\mathrm{true}}{,}{b}{=}{\mathrm{false}}\right\}$ (3)
 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}{=}{-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;
 ${\mathrm{false}}$ (7)

Compatibility

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