# Using Boolean operators in FindInstance

The section on Boolean operators suggests that FindInstance can be applied to them. However, when I try to use it I get a rather confusing error:

Horses :=
(Result == 100 / Speed) &&
((Horse == 1) \[Equivalent] (Speed == 1)) &&
((Horse == 2) \[Equivalent] (Speed == 20))

Result = 5
FindInstance[Horses, {Horse}]


produces the dreaded not a quantified system of equations and inequalities error with no statement of which part is the problem.

Can I not use the relational operator Equivalent in FindInstance, or is what I'm trying to do generally invalid?

• The documentation of FindInstance suggests to me that it can solve satisfiability problems on Boolean statements which contain Boolean-valued variables (I.e. with a True/False value). Your case is trying to solve an algebraic equation with real-valued variables, expressed as a logical statement. I saw no indication that this is possible with FindInstance. Commented Dec 17, 2019 at 4:21
• I saw a comment that <=> isn’t a valid operator. What I actually entered was ESC <=> ESC which I’m not sure how to represent on SO. I’m surprised if using the function call form alone fixes the problem. Commented Dec 17, 2019 at 12:45

Horses := (Result == 100/Speed) &&Equivalent[(Horse == 1), (Speed == 1)] &&
Equivalent[(Horse == 2), (Speed == 20)];Result = 5;
FindInstance[Horses, {Horse, Speed}]


{{Horse -> 2, Speed -> 20}}

• Great. I did have a really bizarre follow-up, though. I then tried change Horse==1 to Horse=="Nag", and Horse==2 to Horse=="Thoroughbred". This caused Mathematica to give a bizarre error message that "the system contains a nonconstant expression Nag", even though Nag should just be a string literal. Even changing it to String["Nag"] didn't stop this error. Weird. Commented Dec 17, 2019 at 20:31
• ... Also, adding && MemberQ[{1,2},Horse] to the Horses system makes it return no instances, even though the instance above makes that true also. Commented Dec 17, 2019 at 20:39