FindInstance

n instances of vars that make expr true, over domain -- scoped to a provably correct core rather than Wolfram's full solver.

✓ checked against that system · ! checked, with disagreements (hover a chip)Wolfram LanguageFindInstance!↗

FindInstance(expr, vars)one instance of vars satisfying expr. Declined here -- the unstated domain is Wolfram's Complexes, outside this scope. See below.

FindInstance(expr, vars, domain)one instance over domain, which must be Reals or Integers.

FindInstance(expr, vars, domain, n)up to n instances over domain.

Typed signatures

Type	Package	Applies
(expression, list<symbol> | symbol, symbol?, integer<1..>?) -> expression	analytic	always

Domain: Relations

Details

• Three provably correct paths, tried in order: a univariate polynomial equation of degree <= 2 with exact integer coefficients, solved by our own quadratic formula -- a COMPLETE real-root enumeration, so when every root fails the rest of the constraints, the conjunction is genuinely infeasible; failing that, compute-engine's Solve as a best-effort finder for equations it happens to solve (never trusted to prove absence); and a bounded integer search, brute-forced over a box whose edges every variable's simple inequalities in expr imply directly.
• Every candidate is re-substituted into every original constraint and re-evaluated before being returned -- the actual safety net, independent of which path produced it.
• An empty result ([]) is only ever returned when infeasibility is proven -- the quadratic route's complete root set, or the bounded search's exhaustive box -- never merely because nothing was found.
• Declines (leaves the call unevaluated) on: the unstated default domain (Complexes); any domain but Reals or Integers; more than one variable without a bounded Integers search; a pure inequality over Reals (no equation, so no provable witness); Or; and an integer search whose bounds are not directly implied by expr's own inequalities.
• Matches Wolfram''s output shape -- a list of rule lists, {{x -> 1}} -- via Rule.

Examples

Basic #

A quadratic with two real roots -- one instance by default

live ↗

In$\mathrm{FindInstance}(x^2=4, x, \mathrm{Reals})$Out$\bigl\lbrack\bigl\lbrack\mathrm{Rule}(x, 2)\bigr\rbrack\bigr\rbrack$

Both roots, with an explicit count

live ↗

In$\mathrm{FindInstance}(x^2=4, x, \mathrm{Reals}, 2)$Out$\bigl\lbrack\bigl\lbrack\mathrm{Rule}(x, 2)\bigr\rbrack, \bigl\lbrack\mathrm{Rule}(x, -2)\bigr\rbrack\bigr\rbrack$

Scope #

An irrational root comes back exact, not a decimal approximation

live ↗

In$\mathrm{FindInstance}(x^2=2, x, \mathrm{Reals})$Out$\bigl\lbrack\bigl\lbrack\mathrm{Rule}(x, \sqrt{2})\bigr\rbrack\bigr\rbrack$

A linear equation

live ↗

In$\mathrm{FindInstance}(2x+3=7, x, \mathrm{Reals})$Out$\bigl\lbrack\bigl\lbrack\mathrm{Rule}(x, 2)\bigr\rbrack\bigr\rbrack$

No real root -- a proven empty result, not a guess

live ↗

In$\mathrm{FindInstance}(x^2=-1, x, \mathrm{Reals})$Out$\bigl\lbrack\bigr\rbrack$

The same equation over Integers -- both roots are irrational, so still proven empty

live ↗

In$\mathrm{FindInstance}(x^2=2, x, ℤ)$Out$\bigl\lbrack\bigr\rbrack$

A bounded integer search -- no equation needed, just inequalities that imply a finite range

live ↗

In$\mathrm{FindInstance}(x\gt0∧x\lt10, x, ℤ, 3)$Out$\bigl\lbrack\bigl\lbrack\mathrm{Rule}(x, 1)\bigr\rbrack, \bigl\lbrack\mathrm{Rule}(x, 2)\bigr\rbrack, \bigl\lbrack\mathrm{Rule}(x, 3)\bigr\rbrack\bigr\rbrack$

A multivariate bounded integer search

live ↗

In$\mathrm{FindInstance}(x+y=5∧x\gt0∧x\lt10∧y\gt0∧y\lt10, \bigl\lbrack x, y\bigr\rbrack, ℤ, 3)$Out$\bigl\lbrack\bigl\lbrack\mathrm{Rule}(x, 1), \mathrm{Rule}(y, 4)\bigr\rbrack, \bigl\lbrack\mathrm{Rule}(x, 2), \mathrm{Rule}(y, 3)\bigr\rbrack, \bigl\lbrack\mathrm{Rule}(x, 3), \mathrm{Rule}(y, 2)\bigr\rbrack\bigr\rbrack$

Finds one real root of the quintic, $x=1$

live ↗

In$\mathrm{FindInstance}(x^5-2x+1=0, x, ℝ)$Out$\bigl\lbrack\bigl\lbrack\mathrm{Rule}(x, 1)\bigr\rbrack\bigr\rbrack$

Possible issues #

Declines without an explicit domain -- the unstated default is Complexes, outside this scope

live ↗

In$\mathrm{FindInstance}(x\gt0, x)$Out$\mathrm{FindInstance}(x\gt0, x)$

Declines on a pure inequality over Reals -- infinitely many witnesses and no provable canonical one

live ↗

In$\mathrm{FindInstance}(x\gt0, x, \mathrm{Reals})$Out$\mathrm{FindInstance}(x\gt0, x, \mathrm{Reals})$

About

Examples	11
Checked against	Wolfram Language 5 agree6 differ
Crosswalk	Wolfram Language

See also: Solve, Rule, Inequality