Initializations (Evaluate this cell first)

Defining the Unconditional Probability Function Pr[•]

Needs["Utilities`Notation`"];

Ω = {{a}, {b}, {c}, {d}, {e}, {f}, {g}, {h}};
X = {{a}, {b}, {d}, {e}};
Y = {{b}, {c}, {e}, {f}};
Z = {{d}, {e}, {f}, {g}};
Notation[¬ α_ ⟺ Complement[Ω, α_]];
Pr[{}] = 0;
Pr[α_] := 
        Plus @@ Flatten[α] //. 
          h -> 1 - (a + b + c + d + e + f + g);

Notation[Pr[α_  |  β_] ⟺ Pr[α_, β_] ]

Pr[α_  |  β_]  := 
        Pr[α ⋂ β]/Pr[β];

Pr[
      X ⋃ (Y ⋂ Z) | ¬ ( 
            X ⋂ Y)]

Defining the PrSAT Function

Off[Solve::"svars"]
Off[Flatten::"normal"]
Off[General::"spell"]
Off[General::"spell1"]
Off[$MaxExtraPrecision::"meprec"]
Off[General::"sign"]
Needs["Algebra`InequalitySolve`"]
Needs["Graphics`InequalityGraphics`"]
𝔼1 = X;
ℍ1 = Y; ℍ2 = Z;

prNR[
          vars_] :=   And @@ ((0 ≤ # ≤ 
                      1) & /@ vars) && 
          Plus @@ vars ≤ 1;

Regular[vars_] :=  
        If[vars == {a, b, c, d, e, f, g, h}, 
          And @@ ((0 < # < 1) & /@ vars) && Plus @@ vars == 1, 
          And @@ ((0 < # < 1) & /@ vars) && 
            Plus @@ vars < 1];

eqsel[inqs_] := 
        Select[inqs, MatchQ[#, x__ == y__] &];

Vars[x_] := 
        Union[Select[
            Flatten[x //. {y_ && z_ -> {y, z}, y_ < z_ -> {y, z}, 
                  y_ > z_ -> {y, z}, y_ == z_ -> {y, z}, 
                  y_ ≥ z_ -> {y, 
                      z}, 
u_ ≤ y_ ≤ 
                      z_ -> {u, y, z}, 
u_ < y_ < 
                      z_ -> {u, y, 
                      z}, 
y_ ≤ z_ -> {y, 
                      z}, y_ + z_ -> {y, z}, 
                  y_ ≠ z_ -> {y, z}, 
                  Rational[y_, z_] -> {y, z}, 
                  Power[y_, z_] -> {y, z}, 
                  Times[y_, z_] -> {y, z}}], 
            Not[NumericQ[#]] &]];

Options[PrSAT] = {PR -> prNR, CONS -> {}};

\(\(PrSAT[ineqs_, 
          opts___] := \((pr = \(PR /. {opts}\) /. Options[PrSAT]; 
          cons = \(CONS /. {opts}\) /. Options[PrSAT]; 
          ClearAll[sol, sol1, ineqs1, model1, model, ms, m, i]; 
          sol1 = Solve[
              eqsel[ineqs] ⋃ 
                cons ⋃ {a ≠ 0, b ≠ 0, 
                  c ≠ 0, d ≠ 0, e ≠ 0, 
                  f ≠ 0, g ≠ 0}]; i = 0; 
          sol[i] = {}; 
While[
            sol[i] == {} && i < Length[sol1], \(i++\); 
            ineqs1[i] = 
              pr[Vars[ineqs]] && 
                  And @@ ineqs //. sol1[[
                  i]]; 
            sol[i] = 
              Developer`InequalityInstance[ineqs1[i], Vars[ineqs1[i]]]; 
            model1[i] = 
              Flatten[Join[
                  sol1[[
                      i]] //. sol[i], 
                  sol[i]]]; 
            model2[i] = 
              Developer`InequalityInstance[
                pr[{a, b, c, d, e, f, g, h}] && 
                    And @@ ineqs //. model1[i], 
                Vars[pr[{a, b, c, d, e, f, g, h}] && 
                      And @@ ineqs //. model1[i]]]; 
            If[model2[i] == {}, \(model[i] = False;\), \(model[i] = 
                  Sort[Join[model1[i], model2[i]]];\)]; 
            ms = If[sol1 == {}, {}, 
                Table[model[i], {i, 1, Length[sol1]}]];]; 
          If[Or @@ ms === False, Print["Unsatisfiable"], 
            Print["Satisfiable: ", 
              Select[ms, ListQ]]];)\);\)\)

The Monty Hall Problem: Animation

LINE[γ_] := 
        Plot[-(((-1 + c) γ)/(1 + γ)), {c, 
            0, 1}, DisplayFunction -> Identity, 
          PlotStyle -> Thickness[ .005]];
LINE1[γ_] := 
        Plot[-(((-1 + c) γ)/(1 + γ)), {c, 
            0, 1}, DisplayFunction -> 
            Identity];
sol = {a -> γ - c γ - d γ, b -> 0, 
        e -> 0, f -> 0, g -> 0, 
        h -> 1 - (a + b + c + d + e + f + g)}; 
    INEQ1 = InequalitySolve[(0 < a < 1 && 0 ≤ b ≤ 1 && 
              0 < c < 1 && 0 < d < 1 && 0 ≤ e ≤ 1 && 
              0 ≤ f ≤ 1 && 
              0 ≤ g ≤ 1 && 
              0 ≤ h ≤ 1 && 
              a + b + c + d + e + f + g + h == 1 && 
              Pr[𝔼1 | ℍ2] > 
                Pr[𝔼1 | ¬ (ℍ1 ⋃ ℍ2)] && 
              Pr[𝔼1 | ¬ ℍ2] ≤ 
                Pr[𝔼1 |  ℍ1 ⋃ ℍ2]) //. sol, {a, b, c, d, e, f, g, 
          h, γ}];
INEQ2 = 
        InequalitySolve[(0 < a < 1 && 0 ≤ b ≤ 1 && 
                0 < c < 1 && 0 < d < 1 && 0 ≤ e ≤ 1 && 
                0 ≤ f ≤ 1 && 
                0 ≤ g ≤ 1 && 
                0 ≤ h ≤ 1 && 
                a + b + c + d + e + f + g + h == 1 && 
                Pr[¬ (ℍ1 ⋃ ℍ2) | 𝔼1] - 
                    Pr[¬ (ℍ1 ⋃ ℍ2)] < 
                  Pr[ℍ2 | 𝔼1] - 
                    Pr[ℍ2]) //. sol, {a, b, c, d, e, 
            f, g, h, γ}];
INEQ3 = 
        InequalitySolve[(0 < a < 1 && 0 ≤ b ≤ 1 && 
                0 < c < 1 && 0 < d < 1 && 0 ≤ e ≤ 1 && 
                0 ≤ f ≤ 1 && 
                0 ≤ g ≤ 1 && 
                0 ≤ h ≤ 1 && 
                a + b + c + d + e + f + g + h == 1 && 
                Pr[𝔼1 | ℍ2]/Pr[𝔼1 | ¬ ℍ2] > 
                  Pr[𝔼1 | ¬ (ℍ1 ⋃ ℍ2)]/Pr[𝔼1 |  ℍ1 ⋃ ℍ2]) //. sol, {a, b, c, d, e, f, g, 
            h, γ}];
IP1[g_] := 
        InequalityPlot[INEQ1 //. γ -> g, {c, 0, 1}, {d, 0, 1}, 
          PlotRange -> {{0, 1}, {0, 1}}, 
          DisplayFunction -> Identity, 
          PlotStyle -> {{RGBColor[1, 0, 0]}}, Curves -> Front, 
          Fills -> {GrayLevel[1]}];
IP2[g_] := 
        InequalityPlot[INEQ2 //. γ -> g, {c, 0, 1}, {d, 0, 1}, 
          PlotRange -> {{0, 1}, {0, 1}}, 
          DisplayFunction -> Identity, 
          PlotStyle -> {{RGBColor[0, 1, 0]}}, Curves -> Front, 
          Fills -> {GrayLevel[1]}];
IP3[g_] := 
        InequalityPlot[INEQ3 //. γ -> g, {c, 0, 1}, {d, 0, 1}, 
          PlotRange -> {{0, 1}, {0, 1}}, 
          DisplayFunction -> Identity, 
          PlotStyle -> {{RGBColor[0, 0, 1]}}, Curves -> Front, 
          Fills -> {GrayLevel[1]}];
pt = 
        Show[Graphics[{AbsolutePointSize[6], Point[{1/3, 1/3}]}], 
          DisplayFunction -> Identity];
Clear[i];
\(\(Table[
        Show[{IP3[i], IP2[i], IP1[i], pt, LINE1[i], LINE[10000], 
            Graphics[
              Text[\*""Pr(E | (Subscript[H, 3])) = "" <> 
                  ToString[i], { .7,  .7}]]}, 
          
          AxesLabel -> {\*""Pr((Subscript[H, 1]))"", \ \*""Pr((Subscript[H, 2]))""}, DisplayFunction -> $DisplayFunction], {i,  .1, 
          1,  .1}];\)\)