En donnant des moyens d'exprimer l'alternation de quantificateurs existentiels et universels, les langages quantifiés permettent de poser formellement des questions dont la réponse est une stratégie. Par exemple, on peut encoder les règles d'un jeu comme un ensemble de contraintes, puis demander l'existence d'une stratégie gagnante (ou au moins nonperdante) pour ce jeu. Dans le cas de formules booléennes quantifiées, une telle stratégie, si elle existe, est représentée par un certificat de satisfiabilité, qui est une représentation compacte d'un des modèles de la formule et qui peut être utilisé pour donner une preuve de satisfiabilité indépendante du solveur. Etant donnée la nature intrinsèque des formules quantifiées, de tels certificats demandent beaucoup de soin pour être extraits efficacement, représentés de façon compacte et pour que l'on puisse aisément leur poser des requêtes. Nous montrons comment résoudre ces problèmes.