One essential step in sequential logic synthesis consists of finding a state encoding that meets some requirements, such as optimal implementation, or correctness in the case of asynchronous FSMs. Dichotomy-based constrained encoding is more general than other constrained encoding frameworks, but it is also more difficult to solve. This paper introduces a new formalization of this problem, which leads to original exact and heuristic algorithms. Experimental results show that the resulting exact solver outperforms the previous approaches.