Earlier today I ran a conda install command, only to have it sit there minutes on end with no apparent progress, so I re-ran it with -vv (uncertain whether it supported verbose output). I saw lots of “invoking SAT with clause count <number goes here>” printed to the terminal.

I know that the Boolean satisfiability problem appears everywhere and is core to solving all sorts of optimization problems, but I did not expect conda to show me so obviously that it’s used in dependency resolution!