\myheading{SAT assumptions} I'm using SAT assumptions. What is this? Imagine you play Doom/Quake/another shooter videogame. You gone far and you stumbled before the fork in the road. You know you may get killed by a monster. So you save the state of the game, you take a first path, you get killed by a monster, you restore a state, you take a second path, etc, etc. You want to save the state because you don't want to lose what you've achieved up to this point. It takes a time for SAT solver to process input clauses, to 'warm up', like an engine. Here I'm using SAT assumption after all the constraints processed, and I 'assume' that a package X has version Y. I execute sat() call of picosat, it returns SAT or UNSAT, and all 'assumptions' are reset after each sat() call, but the picosat SAT solver is still 'warmed up', and all constraints are still there. And then I 'assume' that a package X has version Y-1, and execute sat() call again, etc, etc. It's impossible to add assumptions running picosat executable, so I have to load the libpicosat.so shared library and call all these functions one after another. It's important to note that I could run picosat executable instead, without any assumptions, but then the whole process would be longer: because you'll have to generate CNF file each time, picosat SAT solver have to process all the clauses from the beginning, 'warm its engine', etc.