Clear[validComb,countConstraint,rootConstraint,leafConstraint,getCombs];

outer[lists__]:=(Flatten[Outer[List,lists],Length[{lists}]-1])

g=PathGraph[{1,2}];
k=1;
getChildren[i_]:=Select[VertexList[NeighborhoodGraph[g,i]],#>i&];
isLeaf[i_]:=\[LeftBracketingBar]getChildren[i]\[RightBracketingBar]==0;

(* helper tools to extract information from vertex state *)
vstates=outer[{1,0},Range[0,k]];
occupied[vstate_List]:=(vstate[[1]]==1);
count[vstate_List]:=vstate[[2]];

isValidFactorState[factor_,fstate_]:=(
And[
countCons[factor,fstate],
rootCons[factor,fstate],
leafCons[factor,fstate]
]
);

countCons[factor_,fstate_]:=(
headVState=First[fstate];
childVStates=Rest[fstate];
headCount=count[headVState];
restCount=Total[count/@childVStates];
occupied[headVState]&&(headCount==restCount+1)||!occupied[headVState]&&(headCount==restCount)
);

(* checks if head of factor is root, in which case checks it's set to k *)
rootCons[factor_,fstate_]:=(
head=First[factor];
head$vstate=First[fstate];
head≠1||head==1&&count[head$vstate]==k
);

(* checks if head of factor is leaf, in which case checks if count is set to 0 or 1 *)
leafCons[factor_,fstate_]:=(
head=First[factor];
head$vstate=First[fstate];
!isLeaf[head]||
isLeaf[head]&&(occupied[headState]&&count[head$vstate]==1||!occupied[head$vstate]&&count[head$vstate]==0)
);

(* at least one configuration must be legal *)
factorFormula[factor_]:=(
head=First[factor];
children=Rest[factor];
Assert[getChildren[head]==children];

fstates=Tuples[vstates,\[LeftBracketingBar]factor\[RightBracketingBar]];
valid$fstates=Select[fstates,isValidFactorState[factor,#]&];
factorFormulas=encodeFactorState[factor,#]&/@valid$fstates;
Or@@factorFormulas
);

(* exactly one state must be chosen *)
vertexFormula[vertex_]:=(
(* find formula satisfying assignment *)
);

encodeFactorState[factor_,fstate_]:=(
And@@(encodeVertexState/@Transpose[{factor,fstate}])
);

encodeVertexState[{v_,vstate_}]:=(
If[occupied[vstate],vo[v],!vo[v]]&&vc[v][count[vstate]]
);