# How to simplify Boolean expression

I would like to simplify $$((p\oplus q)=True)\wedge(p=True)$$ to $$q=False$$ I was hoping

BooleanMinimize[((p ⊻ q) == 1) ∧ (p == True)]


would do the trick, but nothing happened. I also tried FullSimplify and Assumptions without luck. How can I do this simplification? This is a specific example, but I would like a method that could handle more complicated cases.

Here are some examples you can test on

((p ⊻ q) == True) ∧ ((p ⊻ q ⊻ r) == True)
(*should give*)
r == False

((p ∧ q) == True) ∧ ((p ⊻ q ⊻ r) == True)
(*should give*)
r == True

(((p ∧ s) ⊻ (q ∧ r)) == True) ∧ ((p ∧ q) == True)
(*should give*)
(s ⊻ r) == True


## 2 Answers

This sort of thing can be recast as a quantifier elimination problem, as below. Quantify the variables you want to remove, set conditions on them as needed, and use Resolve to do the elimination step. A postprocessing step of BooleanMinimize might be needed (not in the examples below though).

Resolve[Exists[p, p == True, p \[Xor] q]]

(* Out[324]= ! q *)

Resolve[
Exists[{p, q}, (p \[And] q) ==
True, (p \[And] s) \[Xor] (q \[And] r)]]

(* Out[325]= r \[Xor] s *)


WRT your first example:

Simplify[Xor[p, q] == True, Assumptions -> p == True]
(*
True == ! q
*)

Not /@ Simplify[Xor[p, q] == True, Assumptions -> p == True]

(*
False == q
*)


Edit

Daniel's answer is probably the way. However just for reference (and because I already did it :) ), here is another more laborious possibility that works OK with your examples:

expr2 = (p ∧ q);
expr1 = ((p ∧ s) ⊻ (q ∧ r));
vars[exp_] := BooleanVariables@exp
res[exp_] :=  Pick[Tuples[{True, False}, Length@vars@exp], BooleanTable[exp, vars@exp]]
f[x_] := Select[res@expr1, #[[;; Length@vars@expr2]] == x &]
tab = (f /@ res@expr2 // First)[[All, Length@vars@expr2 + 1 ;;]];
Simplify@BooleanFunction[Join[Thread[tab->True], {{__}->False}],Complement[vars@expr1, vars@expr2]]

(* r \[Xor] s *)