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.
![](https://0xba.net/wp-content/uploads/2019/06/2019-06-28_15-57-28-1024x347.png)