Pourquoi tous les solveurs SAT récents fonctionnent-ils sur CNF au lieu du circuit SAT?

Question

Après la sortie de la bibliothèque Aiger pour gérer des graphiques et des indexes en 2006 (je pense), certains solveurs SAT de circuit ont été publiés en 2006-2008, et dans quelques courses / compétitions SAT, il y avait des pistes AIG. Cependant, depuis lors, il semble que l'accent soit mis sur le SMT ou l'amélioration des solveurs SAT Clausal.

Intuitivement pour moi, me concentrer sur le circuit SAT semble avoir beaucoup de sens: beaucoup sinon la plupart des problèmes sont plus naturellement exprimés en circuit assis que CNF; Les circuits fournissent des informations structurelles qui ne peuvent pas être inversées à partir de CNF, mais les circuits peuvent toujours être transformés en CNF; Et au moins le domaine de la synthèse logique significativement significatif semble être particulièrement bon pour les AIG.

Alors, qu'est-ce-qu'il s'est passé? Il s'est-il avéré que les informations structurelles supplémentaires n'aident pas les solveurs? SAT basé sur AIG a-t-il résolu une expérience ratée?