FindInstance[expr,vars]
finds an instance of vars that makes the statement expr be True.
FindInstance[expr,vars,dom]
finds an instance over the domain dom. Common choices of dom are Complexes, Reals, Integers, and Booleans.
FindInstance[expr,vars,dom,n]
finds n instances.
FindInstance
FindInstance[expr,vars]
finds an instance of vars that makes the statement expr be True.
FindInstance[expr,vars,dom]
finds an instance over the domain dom. Common choices of dom are Complexes, Reals, Integers, and Booleans.
FindInstance[expr,vars,dom,n]
finds n instances.
Details and Options
- FindInstance[expr,{x1,x2,…}] gives results in the same form as Solve: {{x1->val1,x2->val2,…}} if an instance exists, and {} if it does not.
- expr can contain equations, inequalities, domain specifications and quantifiers, in the same form as in Reduce.
- The statement expr can be any logical combination of:
-
lhs==rhs equations lhs!=rhs inequations lhs>rhs or lhs>=rhs inequalities expr∈dom domain specifications {x,y,…}∈reg region specification ForAll[x,cond,expr] universal quantifiers Exists[x,cond,expr] existential quantifiers - With exact symbolic input, FindInstance gives exact results.
- Even if two inputs define the same mathematical set, FindInstance may still pick different instances to return.
- The instances returned by FindInstance typically correspond to special or interesting points in the set.
- FindInstance[expr,vars] assumes by default that quantities appearing algebraically in inequalities are real, while all other quantities are complex.
- FindInstance[expr,vars,Integers] finds solutions to Diophantine equations.
- FindInstance[expr,vars,Booleans] solves Boolean satisfiability for expr.
- FindInstance[expr,vars,Reals] assumes that not only vars but also all function values in expr are real. FindInstance[expr&&vars∈Reals,vars] assumes only that the vars are real.
- FindInstance[…,x∈reg,Reals] constrains x to be in the region reg. The different coordinates for x can be referred to using Indexed[x,i].
- FindInstance may be able to find instances even if Reduce cannot give a complete reduction.
- By default, every time you run FindInstance with a given input, it will return the same output.
- FindInstance[expr,vars,dom,n] will return a shorter list if the total number of instances is less than n.
- The following options can be given:
-
Method Automatic method to use Modulus 0 modulus to assume for integers RandomSeeding 1234 how to seed randomness WorkingPrecision Infinity precision to use in internal computations
Examples
open all close allBasic Examples (6)
Find a solution instance of a system of equations:
FindInstance[x ^ 2 + y ^ 2 + z ^ 2 == -1 && z ^ 2 == 2x - 5 y, {x, y, z}]Find a real solution instance of a system of equations and inequalities:
FindInstance[x ^ 2 + y ^ 2 + z ^ 2 ≤ 1 && 9z ^ 3 == 2x - 5 y - 7, {x, y, z}, Reals]Find an integer solution instance:
FindInstance[x ^ 2 - 3y ^ 2 == 1 && 10 < x < 100, {x, y}, Integers]Find Boolean values of variables that satisfy a formula:
FindInstance[Xor[a, b, c, d] && (a || b) && !(c || d), {a, b, c, d}, Booleans]FindInstance[x ^ 2 - 3y ^ 2 == 1 && 10 < x < 1000, {x, y}, Integers, 3]Find a point in a geometric region:
FindInstance[{x, y}∈InfiniteLine[{{0, 0}, {2, 1}}] && {x, y}∈Circle[], {x, y}]Graphics[{{Blue, InfiniteLine[{{0, 0}, {2, 1}}], Circle[]}, {Red, Point[{x, y}] /. %}}]Scope (57)
Complex Domain (11)
FindInstance[2 x + 3y - 5z == 1 && 3x - 4y + 7z == 3, {x, y, z}]A univariate polynomial equation:
FindInstance[x ^ 3 - 2x + 1 == 0, x]Five roots of a polynomial of a high degree:
FindInstance[x ^ 1234567 + 9x ^ 2 + 7x - 1 == 0, x, 5]A multivariate polynomial equation:
FindInstance[x ^ 2 - y z == 1, {x, y, z}]Systems of polynomial equations and inequations:
FindInstance[x ^ 2 + y ^ 3 == z && x + 2y == 3z + 1 && x y z ≠ 0, {x, y, z}]This gives three solution instances:
FindInstance[x ^ 2 + y ^ 3 == z && x + 2y == 3z + 1 && x y z ≠ 0, {x, y, z}, 3]If there are no solutions FindInstance returns an empty list:
FindInstance[x ^ 2 + y ^ 3 == 3 && x + 2y == 4 && x y == 5, {x, y}]If there are fewer solutions than the requested number, FindInstance returns all solutions:
FindInstance[x ^ 2 + y ^ 2 == 1 && x == 2y + 1, {x, y}, 5]Five out of a trillion roots of a polynomial system:
FindInstance[x ^ 10000 == y ^ 2 + 3y + 2 && y ^ 10000 == z ^ 2 + 3z + 2 && z ^ 10000 == x ^ 2 + 3x + 2, {x, y, z}, 5]FindInstance[ForAll[x, Exists[y, a x ^ 2 + b y ^ 2 - 3y == 1 && a y ≠ 0]], {a, b}]FindInstance[Sqrt[x + 2y] - 3x + 4y == 5 && x + y ^ (1 / 3) == 1, {x, y}]FindInstance[Sin[x] == 1 / 3, x]FindInstance[ 4 ^ (x ^ 2)2 ^ x == 8, x]In this case there is no solution:
FindInstance[Log[x] == 75 / 11 I Pi + 17, x]A solution in terms of transcendental Root objects:
FindInstance[Sin[Cos[x ^ 2 - 1]] - x == 1 && Abs[x] < 3, x]Five roots of an unrestricted equation:
FindInstance[Sin[FresnelS[x] + BesselJ[3, x ^ 2 - 1]] == 2 ^ Cos[x] - 3, x, 5]Systems of transcendental equations:
FindInstance[Sin[x + y] == 1 / 2 && E ^ x - y == 1, {x, y}]{{x -> Root[{-1 - 2*Sin[1 - E^#1 - #1] & , 0.24542910765918454774059398459939984605`15.15051499783199}], y -> -1 + E^Root[{-1 - 2*Sin[1 - E^#1 - #1] & , 0.24542910765918454774059398459939984605`15.15051499783199}]}}FindInstance[Gamma[x + y + 1] - Sin[x y] == 1 && Erf[x ^ 2 - y] - E ^ y - x + 4 == 0, {x, y}]Three roots of a transcendental system:
FindInstance[Sin[x + y] == x y + 1 && Cos[x - y] == AiryAi[x y] + 2, {x, y}, 3]Real Domain (13)
FindInstance[2 x + 3y - 5z == 1 && 3x - 4y + 7z == 3, {x, y, z}, Reals]A univariate polynomial equation:
FindInstance[x ^ 5 - 2x + 1 == 0, x, Reals]A univariate polynomial inequality:
FindInstance[x ^ 5 - 2x + 1 < 0, x, Reals]A multivariate polynomial equation:
FindInstance[x ^ 2 - y z == 1, {x, y, z}, Reals]A multivariate polynomial inequality:
FindInstance[x ^ 2 - 2y + z ^ 2 ≥ 1, {x, y, z}, Reals]Systems of polynomial equations and inequalities:
FindInstance[x ^ 2 + y z == 1 && x + 2y ≤ 3z + 1 && x y z > 7, {x, y, z}, Reals]FindInstance[x ^ 2 + y z == 1 && x + 2y ≤ 3z + 1 && x y z > 7, {x, y, z}, Reals, 4]If there are no solutions FindInstance returns an empty list:
FindInstance[x ^ 2 + y ^ 3 == 3 && x + 2y ≥ 4 && x y == 5, {x, y}, Reals]If there are fewer solutions than the requested number, FindInstance returns all solutions:
FindInstance[x ^ 2 + y ^ 2 == 1 && x == 2y + 1, {x, y}, Reals, 5]A quantified polynomial system:
FindInstance[ForAll[x, Exists[y, a x ^ 2 + b y ^ 2 - 3y == 1 && y < 0]], {a, b}, Reals]FindInstance[Sqrt[x + 2y] - 3x + 4y ≥ 5 && x + y ^ (1 / 3) == 1, {x, y}, Reals]FindInstance[Abs[(x + Abs[x + 2]) ^ 2 - 1] ^ 2 == 9 && x ≠ 0, x, Reals]FindInstance[Max[x, y] == Min[y ^ 2 - x, x] && x > 0, {x, y}, Reals]FindInstance[Abs[3x ^ 2 - 7x - 6] < Abs[x ^ 2 + x], x, Reals]FindInstance[1 < Floor[x ^ 2 + Ceiling[x ^ 2]] < 10, x, Reals]FindInstance[E ^ x - x == 7, x, Reals]FindInstance[ 27^2x - 1^(1/(x)) == Sqrt[9^2x - 1], x, Reals]A solution in terms of transcendental Root objects:
FindInstance[E ^ x - Log[x] + x ^ 2 == 1, x]FindInstance[1 / 4 < Sin[x] < 1 / 3, x, Reals]FindInstance[ (1/2^x - 1) > (1/1 - 2^x - 1), x, Reals]FindInstance[Sin[x + y] == 1 / 2 && E ^ x - y ≤ 1, {x, y}, Reals]FindInstance[ 3^x - 2^2y == 77 && Sqrt[3^x] - 2^y == 7, {x, y}, Reals]FindInstance[2 ^ z Sin[x + y] == z - 1 && x Gamma[y + z] == Sin[x y] + 1 && z > E ^ x, {x, y, z}, Reals]Integer Domain (12)
FindInstance[2 x + 3y - 5z == 1 && 3x - 4y + 7z == 3, {x, y, z}, Integers]A linear system of equations and inequalities:
FindInstance[2 x + 3y == 4 && 3x - 4y ≤ 5 && x - 2y > -21, {x, y, z}, Integers]FindInstance[2 x + 3y == 4 && 3x - 4y ≤ 5 && x - 2y > -21, {x, y, z}, Integers, 5]A univariate polynomial equation:
FindInstance[x ^ 1000 - 2x ^ 777 + 1 == 0, x, Integers]A univariate polynomial inequality:
FindInstance[x ^ 5 - 2x + 1 < 0, x, Integers]FindInstance[x ^ 2 + x y + y ^ 2 == 109, {x, y}, Integers]FindInstance[x ^ 2 - 3y ^ 2 == 22 && x > 0 && y > 0, {x, y}, Integers]FindInstance[x ^ 2 - 6 x y + 9y ^ 2 - x + 2y == 1, {x, y}, Integers]FindInstance[x ^ 3 - 2x ^ 2 y + y ^ 3 == 2, {x, y}, Integers]If there are fewer solutions than the requested number, FindInstance returns all solutions:
FindInstance[x ^ 3 - 2x ^ 2 y + y ^ 3 == 2, {x, y}, Integers, 3]FindInstance[x ^ 2 + y ^ 2 + z ^ 2 + t ^ 2 == 123456789, {x, y, z, t}, Integers]FindInstance[x ^ 2 + y ^ 2 == z ^ 2 && 100 < x < y < z, {x, y, z}, Integers]A bounded system of equations and inequalities:
FindInstance[x ^ 4 + y ^ 4 + z ^ 4 ≤ 500 && x + y ^ 2 + z ^ 3 == 32, {x, y, z}, Integers]A high-degree system with no solution:
FindInstance[2x ^ 7 + 8y ^ 15 + 14 x y z == 3, {x, y, z}, Integers]Transcendental Diophantine systems:
FindInstance[Exp[y ^ 2] < x && Abs[x] < 5 && Abs[y] < 5, {x, y}, Integers]FindInstance[Exp[x ^ 2 - 5y ^ 2 + 1] + x ^ 2 - 5y ^ 2 == 0 && x > 0 && y > 0, {x, y}, Integers]A polynomial system of congruences:
FindInstance[Mod[x ^ 2 + y ^ 2, 2] == 1 && Mod[x - 2y, 3] == 2, {x, y}, Integers]Modular Domains (5)
FindInstance[2 x + 3y - 5z == 1 && 3x - 4y + 7z == 3, {x, y, z}, Modulus -> 12]A univariate polynomial equation:
FindInstance[x ^ 3 - 2x + 1 == 0, x, Modulus -> 5]A multivariate polynomial equation:
FindInstance[x ^ 2 - y z == 1, {x, y, z}, Modulus -> 4]FindInstance[x ^ 2 - y z == 1, {x, y, z}, 7, Modulus -> 4]A system of polynomial equations and inequations:
FindInstance[x ^ 2 + y ^ 3 == z && x + 2y == 3z + 1 && x y z ≠ 0, {x, y, z}, Modulus -> 7]A quantified polynomial system:
FindInstance[ForAll[x, Exists[y, a x ^ 2 + b y ^ 2 - 3y == 1 && y ≠ 0]], {a, b}, Modulus -> 3]Finite Field Domains (4)
ℱ = FiniteField[53, 4];
FindInstance[x ^ 5 + ℱ[123]x == ℱ[234], x]FindInstance[x ^ 7 + 2 x + 3 == 0, x, ℱ]ℱ = FiniteField[71, 2];
FindInstance[ℱ[123]x + ℱ[234]y == ℱ[345] && ℱ[321]x + ℱ[432]y == ℱ[543], {x, y}]FindInstance[ℱ[1234]x + ℱ[2345]y + ℱ[3456]z == ℱ[4567] && ℱ[1]x + ℱ[2]y + ℱ[3]z == ℱ[4], {x, y, z}]Systems of polynomial equations:
ℱ = FiniteField[7, 5];
FindInstance[x ^ 2 + y ^ 2 + z ^ 2 == 21, {x, y, z}, ℱ]FindInstance[ℱ[321]x ^ 3 + ℱ[432]y ^ 3 + ℱ[543]z ^ 3 == ℱ[654] && x ^ 2 == ℱ[333]y z + ℱ[111], {x, y, z}, 3]Systems involving quantifiers:
ℱ = FiniteField[2, 5];
FindInstance[Exists[z, ℱ[1]x + ℱ[3]y + ℱ[5]z == ℱ[7] && ℱ[21]x + ℱ[23]y + ℱ[25]z == ℱ[27]], {x, y}]FindInstance[Exists[{y, z}, ℱ[1]x ^ 2 + ℱ[2]y ^ 3 + ℱ[3]z ^ 4 == ℱ[4] && ℱ[5]x ^ 4 + ℱ[6]y ^ 3 + ℱ[7]z ^ 2 == ℱ[8] && x y z != ℱ[0]], x]Mixed Domains (3)
Mixed real and complex variables:
FindInstance[x ^ 2 + y ^ 2 == -1 && Element[x, Reals], {x, y}]Find a real value of
and a complex value of
for which
is real and less than
:
FindInstance[x ^ 2 + y ^ 2 < -1 && Element[x, Reals], {x, y}, Complexes]An inequality involving Abs[z]:
pts = {Re[z], Im[z]} /. FindInstance[1 < Abs[ (z - 2/2z - 1)] < 2, z, 7]Block[{z = u + I v}, RegionPlot[1 < Abs[ (z - 2/2z - 1)] < 2, {u, -1, 1}, {v, -1, 1}, Epilog -> {Blue, PointSize[Large], Point[pts]}]]Geometric Regions (9)
Find instances in basic geometric regions in 2D:
Subscript[ℛ, 1] = Circle[];
Subscript[ℛ, 2] = Line[{{-2, 1}, {1, -2}}];FindInstance[{x, y}∈Subscript[ℛ, 1], {x, y}∈Subscript[ℛ, 2]]Graphics[{{Blue, Subscript[ℛ, 1], Subscript[ℛ, 2]}, {Red, Point[{x, y}] /. %}}]Find instances in basic geometric regions in 3D:
Subscript[ℛ, 1] = Sphere[];
Subscript[ℛ, 2] = InfinitePlane[{{0, 0, 0}, {0, 1, 0}, {1, 0, 1}}];FindInstance[2 x y ≤ z^2 && {x, y, z}∈Subscript[ℛ, 1] && {x, y, z}∈Subscript[ℛ, 2], {x, y, z}, Reals]Show[{ContourPlot3D[2 x y == z^2, {x, -1.2, 1.2}, {y, -1.2, 1.2}, {z, -1.2, 1.2}, Mesh -> None, ContourStyle -> Opacity[0.5]], Graphics3D[{{Opacity[0.5], Green, Subscript[ℛ, 1]}, {Opacity[0.5], Yellow, Subscript[ℛ, 2]}, {PointSize[Large], Red, Point[{x, y, z} /. %]}}]}]Find a point in the projection of a region:
ℛ = Cone[{{1, 2, 3}, {3, 2, 1}}, 1];FindInstance[Subscript[∃, z]{x, y, z}∈ℛ, {x, y}, Reals, 100];Graphics3D[{{Green, ℛ}, {Red, Point[{x, y, 0} /. %]}}]ℛ = ImplicitRegion[a + 2 b - 3 c ≥ 1 && a b c == 7, {a, b, c}];FindInstance[{x, y, z}∈ℛ, {x, y, z}, Reals]A parametrically defined region:
ℛ = ParametricRegion[{s + t, s - t, s t}, {s, t}];FindInstance[x y > z && {x, y, z}∈ℛ, {x, y, z}, Reals]Subscript[ℛ, 1] = Disk[{0, 0}, 2];
Subscript[ℛ, 2] = Circle[{1, 1}, 2];
Subscript[ℛ, 3] = RegionIntersection[Subscript[ℛ, 1], Subscript[ℛ, 2]];FindInstance[x^2 ≥ x y + 1, {x, y}∈Subscript[ℛ, 3]]Show[{RegionPlot[x^2 ≥ x y + 1, {x, -2, 3}, {y, -2, 3}], Graphics[{{Opacity[0.5], Yellow, Subscript[ℛ, 1]}, {Green, Subscript[ℛ, 2]}, {Red, Point[{x, y} /. %]}}]}]Regions dependent on parameters:
Subscript[ℛ, 1] = InfiniteLine[{{2, 0}, {0, t}}];
Subscript[ℛ, 2] = Circle[];FindInstance[Subscript[∃, {x, y}]({x, y}∈Subscript[ℛ, 1] && {x, y}∈Subscript[ℛ, 2]), t, Reals]Find values of parameters
,
, and
for which the circles contain the given points:
Subscript[ℛ, 1] = Circle[{a, b}, r];
Subscript[ℛ, 2] = Circle[{a + 1, b}, r];
Subscript[ℛ, 3] = RegionIntersection[Subscript[ℛ, 1], Subscript[ℛ, 2]];FindInstance[({0, 1} | {0, -1})∈Subscript[ℛ, 3], {a, b, r}, Reals]Show[{Graphics[{{Blue, Subscript[ℛ, 1]}, {Green, Subscript[ℛ, 2]}, {Red, Point[{{0, 1}, {0, -1}}]}} /. %]}]Use
to specify that
is a vector in
:
ℛ = RegionIntersection[Circle[], Line[{{-2, -1}, {1, 2}}]];FindInstance[x∈ℛ, x]ℛ = Sphere[];FindInstance[x.{1, 2, 3} == 0 && x.{-3, -2, -1} < 0, x∈ℛ]Options (4)
Method (1)
This locally sets system options in "InequalitySolvingOptions" and "ReduceOptions" groups:
FindInstance[2 x + 3 y z + 4 z^2 t ≤ 1 && 5 t^3 y + 7 z^4 - 4 t^3 + 4 z^2 t^2 ≤ 3 && 3 x - 5 t z^2 - 3 t^2 - y z t ≥ 2 && t^2 + z^2 ≤ z y, {x, y, z, t}, Method -> {"LWPreprocessor" -> False}]//AbsoluteTimingThe default method, using the Loos–Weispfenning algorithm to eliminate
, is slightly slower here:
FindInstance[2 x + 3 y z + 4 z^2 t ≤ 1 && 5 t^3 y + 7 z^4 - 4 t^3 + 4 z^2 t^2 ≤ 3 && 3 x - 5 t z^2 - 3 t^2 - y z t ≥ 2 && t^2 + z^2 ≤ z y, {x, y, z, t}]//AbsoluteTimingModulus (1)
RandomSeeding (1)
Finding instances often involves random choice from large solution sets:
FindInstance[x ^ 2 + y ^ 2 ≤ 1, {x, y}, 3]By default, FindInstance chooses the same solutions each time:
FindInstance[x ^ 2 + y ^ 2 ≤ 1, {x, y}, 3]Use RandomSeedingAutomatic to generate potentially new instances each time:
FindInstance[x ^ 2 + y ^ 2 ≤ 1, {x, y}, 3, RandomSeeding -> Automatic]WorkingPrecision (1)
Finding an exact solution to this problem is hard:
TimeConstrained[FindInstance[x ^ 77 + 3x - 11 == E && y ^ 5 - x ^ 2 y + 21 == Pi && x ^ 2y ^ 3 + z ^ 4 == E ^ Pi, {x, y, z}, Reals], 60]With a finite WorkingPrecision, FindInstance is able to find an approximate solution:
FindInstance[x ^ 77 + 3x - 11 == E && y ^ 5 - x ^ 2 y + 21 == Pi && x ^ 2y ^ 3 + z ^ 4 == E ^ Pi, {x, y, z}, Reals, WorkingPrecision -> 100]//TimingApplications (11)
Geometric Problems (6)
The region ℛ is a subset of if
is empty. Show that Disk[{0,0},{2,1}] is a subset of Rectangle[{-2,-1},{2,1}]:
ℛ = Disk[{0, 0}, {2, 1}];
𝒮 = Rectangle[{-2, -1}, {2, 1}];FindInstance[{x, y}∈RegionDifference[ℛ, 𝒮], {x, y}, Reals]Graphics[{{LightRed, EdgeForm[Gray], 𝒮}, {LightBlue, EdgeForm[Gray], ℛ}}]Show that Rectangle[] is a not a subset of Disk[{0,0},7/5]:
ℛ = Rectangle[];
𝒮 = Disk[{0, 0}, 7 / 5];FindInstance[{x, y}∈RegionDifference[ℛ, 𝒮], {x, y}, Reals]Graphics[{{LightRed, EdgeForm[Gray], 𝒮}, {LightBlue, EdgeForm[Gray], ℛ}, {Red, Point[{x, y} /. %]}}]Show that Cylinder[]⊆Ball[{0,0,0},2]:
ℛ = Cylinder[];
𝒮 = Ball[{0, 0, 0}, 2];FindInstance[{x, y, z}∈RegionDifference[ℛ, 𝒮], {x, y, z}, Reals]Graphics3D[{{Opacity[0.3], 𝒮}, {LightBlue, EdgeForm[Gray], ℛ}}]Show that Cylinder[]⊈Ball[{0,0,0},7/5]:
ℛ = Cylinder[];
𝒮 = Ball[{0, 0, 0}, 7 / 5];FindInstance[{x, y, z}∈RegionDifference[ℛ, 𝒮], {x, y, z}, Reals]Graphics3D[{{Opacity[0.3], 𝒮}, {LightBlue, Opacity[0.3], EdgeForm[Gray], ℛ}, {Red, PointSize[Large], Point[{x, y, z} /. %]}}]Find a point in the intersection of two regions:
p = {x, y} /. FindInstance[x ^ 2 - y ^ 3 ≤ 2 && x ^ 2 + (y + 2) ^ 2 ≤ 1, {x, y}]r1 = RegionPlot[x ^ 2 - y ^ 3 ≤ 2, {x, -3, 3}, {y, -3, 3}, PlotStyle -> Directive[Opacity[0.5], Hue[0.3]]];
r2 = RegionPlot[x ^ 2 + (y + 2) ^ 2 ≤ 1, {x, -3, 3}, {y, -3, 3}, PlotStyle -> Directive[Opacity[0.5], Hue[0.7]]];Show[{r1, r2, Graphics[{Red, PointSize[Large], Point[p]}]}]Find a counterexample to a geometric conjecture:
triangle = a > 0 && b > 0 && c > 0 && a + b > c && a + c > b && b + c > a;
s = 1 / 2(a + b + c);
F = Sqrt[s(s - a)(s - b)(s - c)];
conjecture = 27(b ^ 2 + c ^ 2 - a ^ 2) ^ 2(a ^ 2 + c ^ 2 - b ^ 2) ^ 2(a ^ 2 + b ^ 2 - c ^ 2) ^ 2 ≤ (4F) ^ 6;FindInstance[triangle && !conjecture, {a, b, c}, Reals]Prove the conjecture using stronger assumptions:
acute = a ^ 2 + b ^ 2 > c ^ 2 && a ^ 2 + c ^ 2 > b ^ 2 && b ^ 2 + c ^ 2 > a ^ 2;FindInstance[triangle && acute && !conjecture, {a, b, c}, Reals]Boolean Problems (2)
Prove that a statement is a tautology:
statement = (a && ((a && !(b || (a && c))) || b || (a && c))) || !a || !((a && !(b || (a && c))) || b || (a && c));FindInstance[!statement, {a, b, c}, Booleans]This can be proven with TautologyQ as well:
TautologyQ[statement]Show that a statement is not a tautology; get a counterexample:
statement = (b && ((a && !(b || (a && c))) || b || (a && c))) || !a || !((a && !(b || (a && c))) || b || (a && c));FindInstance[!statement, {a, b, c}, Booleans]This can be done with SatisfiabilityInstances as well:
SatisfiabilityInstances[!statement, {a, b, c}]Integer Problems (3)
FindInstance[x ^ 2 + y ^ 2 == 5 ^ 2 && y > x > 0, {x, y}, Integers]Find Pythagorean triples when they exist:
Table[z -> FindInstance[x ^ 2 + y ^ 2 == z ^ 2 && y > x > 0, {x, y}, Integers], {z, 30}]Two instances are now found when
:
Table[z -> FindInstance[x ^ 2 + y ^ 2 == z ^ 2 && y > x > 0, {x, y}, Integers, 10], {z, 30}]Find Pythagorean quadruples and visualize the result:
FindInstance[x ^ 2 + y ^ 2 + z ^ 2 == 1 ^ 2, {x, y, z}, Integers, 1000]Generate all solutions for
and visualize the result:
sol = Table[FindInstance[x ^ 2 + y ^ 2 + z ^ 2 == d ^ 2, {x, y, z}, Integers, 1000], {d, 20}];Graphics3D[Point[{x, y, z}] /. sol]Show that there are no 2×2 magic squares with all numbers unequal:
FindInstance[a + c == b + d == a + b == c + d && a ≠ b ≠ c ≠ d, {a, b, c, d}, Integers]Properties & Relations (10)
Solution instances satisfy the input system:
system = x ^ 2 + y ^ 2 + z ^ 2 ≤ 1 && x ^ 2 - y ^ 3 + 2z ≤ 3;system /. FindInstance[system, {x, y, z}, 7]Use RootReduce to prove that algebraic numbers satisfy equations:
system = x ^ 2 + y ^ 3 + 2x y == 1;system /. FindInstance[system, {x, y}, 2]RootReduce[%]When there are no solutions, FindInstance returns an empty list:
FindInstance[x ^ 2 + y ^ 2 < 0, {x, y}, Reals]If there are fewer solutions than the requested number, FindInstance returns all solutions:
FindInstance[x ^ 2 - 1 == 0, x, 3]To get a complete description of the solution set use Reduce:
Reduce[x ^ 2 + y ^ 2 + z ^ 2 ≤ 1 && x ^ 2 - y ^ 3 + 2z ≤ 3, {x, y, z}, Reals]Reduce[a x ^ 2 + b x + c == 0, x]To get a generic solution of a system of complex equations use Solve:
Solve[a x ^ 2 + b x + c == 0, x]Solving a sum of squares representation problem:
FindInstance[x ^ 2 + y ^ 2 + z ^ 2 == 12345678, {x, y, z}, Integers]Use SquaresR to find the number of solutions to sum of squares problems:
SquaresR[3, 12345678]Solving a sum of powers representation problem:
FindInstance[x ^ 3 + y ^ 3 + z ^ 3 == 1234567 && x > 0 && y > 0 && z > 0, {x, y, z}, Integers]Use PowersRepresentations to enumerate all solutions:
PowersRepresentations[1234567, 3, 3]Find instances satisfying a Boolean statement:
statement = (a || b || c) && (!a || !b || !c);FindInstance[statement, {a, b, c}, 2]Use SatisfiabilityInstances to obtain solutions represented as Boolean vectors:
SatisfiabilityInstances[statement, {a, b, c}, 2]FindInstance shows that the polynomial
is non-negative:
f = x ^ 2 + 2y ^ 2 + 3 z ^ 2 - x y - x z - y z;FindInstance[f < 0, {x, y, z}]Use PolynomialSumOfSquaresList to represent
as a sum of squares:
PolynomialSumOfSquaresList[f, {x, y, z}]f - %.%//ExpandThe Motzkin polynomial is non-negative, but is not a sum of squares:
m = x ^ 4 y ^ 2 + x ^ 2 y ^ 4 - 3 x ^ 2 y ^ 2 + 1;FindInstance[m < 0, {x, y}]PolynomialSumOfSquaresList[m, {x, y}]Neat Examples (1)
Integer solutions for a Thue equation:
pts = {x, y} /. FindInstance[x ^ 4 - 4 x ^ 3 y - x ^ 2 y ^ 2 + 4 x y ^ 3 + y ^ 4 == 1, {x, y}, Integers, 100]ContourPlot[x ^ 4 - 4 x ^ 3 y - x ^ 2 y ^ 2 + 4 x y ^ 3 + y ^ 4 == 1, {x, -10, 10}, {y, -10, 10}, Epilog -> {PointSize[Large], Red, Point[pts]}]See Also
Solve Reduce RandomSeeding FindRoot AsymptoticSolve PowersRepresentations IntegerPartitions Minimize RegionPlot RegionPlot3D CylindricalDecomposition SemialgebraicComponentInstances ChineseRemainder Resolve SatisfiabilityInstances PolynomialSumOfSquaresList
Function Repository: PolynomialSystemInfeasibilityCertificate
History
Introduced in 2003 (5.0) | Updated in 2014 (10.0) ▪ 2017 (11.2) ▪ 2024 (14.0)
Text
Wolfram Research (2003), FindInstance, Wolfram Language function, https://reference.wolfram.com/language/ref/FindInstance.html (updated 2024).
CMS
Wolfram Language. 2003. "FindInstance." Wolfram Language & System Documentation Center. Wolfram Research. Last Modified 2024. https://reference.wolfram.com/language/ref/FindInstance.html.
APA
Wolfram Language. (2003). FindInstance. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/FindInstance.html
BibTeX
@misc{reference.wolfram_2026_findinstance, author="Wolfram Research", title="{FindInstance}", year="2024", howpublished="\url{https://reference.wolfram.com/language/ref/FindInstance.html}", note=[Accessed: 13-June-2026]}
BibLaTeX
@online{reference.wolfram_2026_findinstance, organization={Wolfram Research}, title={FindInstance}, year={2024}, url={https://reference.wolfram.com/language/ref/FindInstance.html}, note=[Accessed: 13-June-2026]}