Cet article propose d'étendre la génération automatique d'un ensemble de règles de propagation booléenne quantifiée basée sur les littéraux à partir de la table de vérité d'un opérateur logique binaire à la génération automatique d'un compilateur prenant en entrée la table de vérité d'un opérateur logique binaire et offrant en sortie un solveur pour formules booléennes quantifiées prénexes non-FNC.