I'm not extremely proficient with counting complexity classes, but since #SAT is #P-complete, it's decision version, let's call it #SAT(D) (is the number of solutions less than some $k$), is in PSPACE. So there is a reduction from #SAT(D) to TQBF. This reduction should produce a QBF sentence that is true iff a given SAT instance has less than a given number $k$ of solutions.

But is there any known concrete translation to obtain such a QBF sentence? That is, a direct algorithm to encode #SAT(D) instances as equivalente QBF sentences?

I don't mean necessarily something usable in practice to solve #SAT with QBF solvers, but at least some effective encoding.

I'm not extremely proficient with counting complexity classes, but since #SAT is #P-complete, its decision version, let's call it #SAT(D) (is the number of solutions less than some $k$), is in PSPACE. So there is a reduction from #SAT(D) to TQBF. This reduction should produce a QBF sentence that is true iff a given SAT instance has less than a given number $k$ of solutions.

But is there any known concrete translation to obtain such a QBF sentence? That is, a direct algorithm to encode #SAT(D) instances as equivalente QBF sentences?

I don't mean necessarily something usable in practice to solve #SAT with QBF solvers, but at least some effective encoding.