(* PRELIMINARY FUNCTIONS *)
(* Preprocess Boolean expressions *)
STR[F_]:=Module[{S},S=ToString[F];S=StringReplace[S,{"{"->" { ","}"->" } ",","->" , ","!"->" ! ","&&"->" && ","||"->" || ","("->" ( ",")"->" ) "}];
Return[" "<>StringReplace[S," "..->"  "]<>" "]];
(* Transform strings into symbolic expressions and simplify *)
SIM[{VV_,FF_}]:=Module[{i,n,SS},n=Length[FF];SS=ToExpression[FF];Return[{VV,Map[ToString,BooleanMinimize[FullSimplify[SS]]]}]];
(* Remove variable v and return string *)
DEL[{VV_,FF_},v_]:=Module[{i,n,S,k},n=Length[FF];S={};For[i=1,i≤n,i++,AppendTo[S,STR[FF[[i]]]]];
k=Position[VV,v];If[k=={},(*Print["ERROR"];*)Return[{VV,FF}],k=k[[1,1]]];If[StringPosition[S[[k]]," "<>v<>" "]≠{},Return[{VV,FF}]];(*Print[S];*)
For[i=1,i≤n,i++,If[i==k,Continue[]];S[[i]]=StringReplace[S[[i]]," "<>v<>" "->"( "<>S[[k]]<>" )"]];
Return[{Drop[VV,{k}],Drop[S,{k}]}]
]

(* FUNCTIONS FOR REDUCTION *)
(* Remove variable v and return simplified symbolic expression *)
REMOVEVERTEX[{VV_,FF_},v_]:=SIM[DEL[{VV,FF},v]]
(* Remove one vertex only: try x1 first (forward) *)
REDUCEonestepF[{VV_,FF_}]:=Module[{V,F,n,i,b},
n=Length[VV];{V,F}={VV,FF};
For[i=1,i≤n,i++,{V,F}=SIM[DEL[{V,F},V[[i]]]]; If[Length[V]<n,Return[{V,F}]]];
Return[{V,F}]];
(* Remove one variable only: try xn first (backward) *)
REDUCEonestepB[{VV_,FF_}]:=Module[{V,F,n,i},
n=Length[VV];{V,F}={VV,FF};
For[i=n,i≥1,i=i-1,{V,F}=SIM[DEL[{V,F},V[[i]]]]; If[Length[V]<n,Return[{V,F}]]];
Return[{V,F}]];
(* Remove all removable variables: try x1 first (forward) *)
REDUCEALLF[{VV_,FF_}]:=Module[{V,F,n,i},n=Length[VV];{V,F}=REDUCEonestepF[{VV,FF}]; While[n>Length[V],n=Length[V];{V,F}=REDUCEonestepF[{V,F}]];
Return[{V,F}]];
(* Remove all removable variables: try xn first (backward) *)
REDUCEALLB[{VV_,FF_}]:=Module[{V,F,n,i},n=Length[VV];{V,F}=REDUCEonestepB[{VV,FF}]; While[n>Length[V],n=Length[V];{V,F}=REDUCEonestepB[{V,F}]];
Return[{V,F}]];
(*We have two ways of reducing, "forward" reduction and "backward" reduction*)