Depuis quelques années, la résolution des formules booléennes quantifiées (QBF) est devenu un domaine de recherche important et attractif. En effet, de nombreuses classes de problèmes peuvent être formulées efficacement en des instances QBF (planification, raisonnement non monotone, model checking). Beaucoup de solveurs ont été proposé. La majorité d'entre eux explorent un arbre de recherche en utilisant des techniques basés sur la procédure DLL. Or, les quantificateurs des formules QBF imposent un ordre partiel d'affectation des variables. Pour passer outre cette imposition, nous proposons une nouvelle approche symbolique (QBdd(SAT)). Elle utilise de façon originale les diagrammes de décision binaires pour représenter l'ensemble des modèles (ou impliquants premiers) de la formule booléenne en utilisant des algorithmes de recherches pour SAT. Deux extensions améliorent notre approche. Tout d'abord, nous introduisons un opérateur de réduction sur les BDD afin de limiter leur taille et de pouvoir répondre à la question de la validité des formules QBF. Ensuite, grâce à des nogoods générés à partir du BDD, des coupures sont réalisés dans l'arbre de recherche. En utilisant des techniques basées sur DLL (resp. recherche stochastique), notre approche peut facilement donner lieu à un solveur complet QBdd(DLL) (resp. incomplet QBdd(LS)). Les premières expérimentations montrent de bonnes performances de ces deux solveurs sur certaines classes d'instances de l'évaluation QBF03.