For example, there's an implementation based on satisfiability modulo theories (SMT) available here: https://github.com/HyVar/gentoo_to_mspl