Comment savoir si un solveur SAT progresse dans sa tentative de réfuter une formule ? S’il a franchi une étape vers une réfutation ? Si la déduction qu’il vient de produire sera vraiment utile ? Si les déductions produites vont s’agréger de manière efficace ? Ces questions me hantent depuis des années, pour ne pas dire des décennies.
