Les solveurs SAT actuels sont hautement optimisés et capables d'exploiter la structure des problèmes. Ils sont très rapides sur la plupart des problèmes (mais ils ne peuvent pas être rapides sur tous, car le SAT est difficile).
Ainsi, en compilant votre problème de planification en une instance de SAT, vous êtes en mesure d'exploiter tout le travail qui a été consacré au développement des solveurs SAT modernes. Vous perdrez probablement une certaine structure liée au problème de planification, que vous auriez pu exploiter en écrivant directement un planificateur.
Peut-être qu'en compilant intelligemment le problème de planification et en exploitant la structure de planification à cette étape, vous pourrez obtenir des instances SAT plus faciles. Mais en procédant ainsi, on pourrait dire que vous essayez de résoudre à nouveau le problème de planification, simplement au moyen d'un autre modèle de calcul (un solveur SAT au lieu d'une machine à mémoire vive ou plus indirectement LISP, peu importe).
Alors pourquoi pas TQBF ?
Évidemment, parce que personne n'a encore essayé (ce que je ne peux pas confirmer). Peut-être que personne n'a eu cette idée avant ou peut-être que personne n'a pensé que les solveurs TQBF actuels sont assez intelligents pour résoudre rapidement les problèmes de planification compilés - au moins plus rapidement que les planificateurs de pointe.
Je ne suis pas bien informé sur le milieu des résolveurs de TQBF. En fait, je n'ai jamais entendu parler de quelque chose comme un solveur général de TQBF (à l'exception de la programmation logique en général). Je pense que c'est beaucoup plus difficile à faire que SAT (ce qui n'a pas encore été prouvé, en supposant que Deolalikar ait tort).
Alors, allez-y, essayez-le. Vous pouvez poster un lien vers votre publication ici si vous réussissez.
