A choice function over a set $E$ is a function $f$ that assigns to every
non-empty subset of $E$ one of its elements (of the subset). If $E$ is in fact a
$Σ$-structure, we say that $f$ is regular if it can be defined by an
MSO[$\Sigma$] formula $\varphi(X,x)$, where the first variable $X$ refers to
subsets, and the second variable $x$ i.e. refers to elements.
Naturally, if a $Σ$-structure admits a well-order which can be defined by
an MSO[$\Sigma$] formula $\psi(x,y)$, then one can define such a choice function
$\varphi(X,x)$ that says "I take the least element of X with respect to $\psi$".
The problem, originally stated in my PhD, asks if the reciprocal is true: if a $Σ$-structure $E$ admits a regular choice function $\varphi(X,x)$, does it necessarily also admit a regular well order $\psi(x,y)$?
I conjecture that it is the case. Moreover, I have also hope for a strengthened constructive version, stated as follow:
Conjecture: Let $\Sigma$ be a signature. There exists a procedure that inputs an MSO[$\Sigma$] formula $\varphi(X,x)$ and outputs another one, $\psi(x,y)$, such that for every $Σ$-structure $E$, if $\varphi(X,x)$ is a regular choice function over $E$ then $\psi(x,y)$ is a regular well order over $E$.