Given a system of inequalities, how to make Solve find out that two variables should be equal?

Question

Given two boolean variables x1 and x2 (in the sense that they are in the range [0,1]), if I try to solve the following equation system with Solve:

Solve[{x1 == 1 - x2, x2 == 1 - x1}]

Mathematica will output:

{{x2 -> 1 - x1}}

I am aware that Solve is not treating the variables as boolean, but the statement that x2 can be replaced by the expression 1 - x1 is what I am interested in.

If, instead, I provide Solve with a system of inequalities:

Solve[{x1 != 1 - x2, x2 != 1 - x1}]

Mathematica will output the following error message:

Solve::fulldim: The solution set contains a full-dimensional component; use Reduce for complete solution information. >>

If I try to restrain the variable values in the system:

Solve[{x1 != 1 - x2, x2 != 1 - x1, 0 <= x1 <= 1, 0 <=  x2 <= 1}, Integers]

Mathematica will correctly Solve the system:

{{x1 -> 0, x2 -> 0}, {x1 -> 1, x2 -> 1}}

But this is not the response I am interested in. The output I am looking for is

{{x1 -> x2}}

Since it is a logical conclusion that could be made by just looking at the system and knowing the variables are in the range [0,1].

Is there a way to make solve obtain the output {{x1 -> x2}} instead of the variable values? Or any other function besides Solve that would give me that result?

Answer 1

I guess you are looking for this.

Solve[x1 == !x2 && x2 == !x1, x1] // Quiet

{{x1 -> ! x2}}

I transpose Unequal to Not Equal like following code.

Solve[x1 != !x2 && x2 != !x1
   /. a_ != b_ :> (!a) == b, x1] // Quiet

{{x1 -> x2}}

Answer 2

Unless I'm misunderstanding your question, I think its worth pointing out that

{{x1 -> x2}}

is not a valid solution to your original equation. Indeed, if x1 == x2, then $$x_1=1-x_2=1-x_1$$ which is always false modulo 2. Mathematica's solution

{{x2 -> 1 - x1}}

is correct since the two original equations are not linearly independent, and thus there is only one variable that can be eliminated.

To explicitly solve over the Booleans, you can tell Solve or Reduce to compute modulo 2:

Reduce[{x1 == 1 - x2, x2 == 1 - x1}, Modulus -> 2]

which gives

x1 == 1 + C[1] && x2 == C[1]

which you can verify is true for both C[1] == 0 and C[1] == 1.