(* xor counter stores counts as c[1],c[2],c[3], unary counter uses number of True vales in list *)
equalityConstraint[xorCounter_,unaryCounter_,maxk_]:=(
Or@@Table[xorCounter[k]&&BooleanCountingFunction[{k},unaryCounter],{k,0,maxk}]
);

(* visualizes formula in disjunctive normal form *)
makeEdge[factor_,var_]:=If[Head[var]===Not,factor->var[[1]],factor->var]
visualizeFormula[formula_]:=(
{factors,vars}=formula2cnf[formula];
edges=fl1@table[f∈factors,makeEdge[f,#]&/@f];
vsf=(#->"Square"&/@factors)∼(#->"Circle"&/@vars);

isNegated[a_->b_]:=MemberQ[a,Not[b]];
makeEdgeStyle[edge_]:=edge->If[isNegated[edge],Red,Blue];
edgeStyles=table[e∈edges,e->Directive[Thick,If[isNegated[e],ColorData["Crayola"]["WildWatermelon"],ColorData["Crayola"]["WildBlueYonder"]]]];

vlabels=#->Placed[ToString[#],Tooltip]&/@(factors∼vars);

Graph[edges,VertexShapeFunction->vsf,EdgeStyle->edgeStyles,VertexLabels->vlabels,ImagePadding->40]
);

(* converts boolean formula to CNF form, extracts variables *)
formula2cnf[formula_]:=(
cnfForm=BooleanConvert[formula,"CNF"]/.{And->List,Or->List};
factors=Select[cnfForm,Head[#]==List&];
vars=Flatten[factors]/.Not->Identity;
{factors,Union[vars]}
);

visualizeFormula[equalityConstraint[xor,{b1,b2,b3,b4},4]]