# pkg upgrade -v -r FreeBSD Updating FreeBSD repository catalogue... FreeBSD repository is up to date. FreeBSD is up to date. vulnxml file up-to-date Checking for upgrades (1 candidates): . done Processing candidates (1 candidates): . done Cannot solve problem using SAT solver, trying another plan Checking integrity... done (0 conflicting) Your packages are up to date. --- What causes this warning? What kind of problem has the "SAT solver"? This kind of warning is for no use as nowhere an explanation can be found. At least the package(s) should be shown which are causing the problem. Also more verbosity should be provided which "other plan" is used. --- Hints how to solve this issue is highly appreciated. Thank you.
this is informational, pkg tried itself another plan and figure it has nothing to do in your case. I can probably improve the message, I am open for better wording ;)
(In reply to Baptiste Daroussin from comment #1) > pkg tried itself another plan and figure it has nothing to do in your case. This error/warning stayed unsolved over repeated runs over several days suggesting to me that there is a problem in the database that does not get healed. As no hint is given which packages are affected I deleted several with a lot of dependencies. After each deletion of a package I did run pkg autoremove and then pkg upgrade. The error did not go away. Having culled half of my packages I did a final pkg delete -a then pkg upgrade (where pkg was the only one installed). The error was gone! After pkg install with my list of packages more than 6GB were downloaded and after that a pkg upgrade showed this error no more. What does that tell you? That "SAT solver, trying another plan" did not solve anything. A cryptic message that points to a problem but not helpful at all. So yes, thank you for looking into this and hopefully improving the message.
(In reply to p5B2EA84B3 from comment #2) And improving the SAT solver, of course. :)
ok I see, and sorry for the incovenience I'll see what I can do to improve it (this won't be my highest priority, I prefer to clarify it, as I would love to have enough to tackle all the issues in my todo list, but I don't :() as for improving the sat solver, we are using minisat a pretty standard sat solver, this is not imho the sat solver we should improve but the way we describe the problem to the sat solver, which clearly can be improved.
(In reply to p5B2EA84B3 from comment #3) The Boolean Satisfiability Problem was the first to be proven to be nondeterministic polynomial-time complete (Np-complete): the Cook–Levin theorem. It is still not known if such problems can be always be solved in polynomial time. So, as stands, there is no known general fix that would always complete in a reasonable time frame. It is unlikely that having some "SAT solver" failures problem will complete go way any time soon. Knowing of a failure to find an example that satisfies the dependency constraints might be needed to help explain any oddities associated with what then happens. To try to always give reasons for such a failure likely end up back in the NP-complete type of problem issue. I might suggest the wording not rely on folks guessing what "SAT solver" refers to or is for. More like, say: Could not solve the dependency constraints via the minisat "SAT solver", trying another plan which may at least be more suggestive to more folks reading it. Lack of such a message implicitly indicates that the dependency constraints were proven satisfiable by by minisat providing an example solution. (This avoids output for most usage of minisat.) In other words: I find the message useful but that it could be made less dependent on some jargon .
Thank you Baptiste, Mark for your contribution. To me this is still not satisfactory. I still do not know what purpose that sentence has: “Cannot solve problem using SAT solver, trying another plan.” Is is it an error, a warning, an info or something else? If you start reading such text on a box and it looks that you have a persisting problem. This is nothing that can be ignored and you start trying to make this problem go away. But if that is only a info that the solver just needs a little more time, a subsequent “solved” or “successfully completed” needs to be printed also. And if that takes only a few seconds I probably won’t want to see such message at all, maybe in verbose mode. Now the most important is: Was the pkg sqlite database ever in a critical state, that would have needed an action? To me it looked like this, finally resulting in a pkg delete -a. How else could this have been solved without touching a single package and avoiding mass downloading, just for getting a sane order of packages? Something like reinstall all in a dry mode but writing new tables or indexes to the database could have done it. I still do not know what kind of beast this was. Was my action necessary, appropriate? From an admin’s or user’s view you should not need to lookup what a propositional satisfiability problem is and guess if this might bite you at some time later.
(In reply to p5B2EA84B3 from comment #6) Also having a prefix indicating the informational status that bapt has noted here could work, say something like: Informational note: Could not solve the dependency constraints via the minisat "SAT solver", so trying a different way of handling the dependency related ordering. It may well be that minisat is non-determistic in some of its techniques for exploring the solution space. (Also fits with dependency constraints commonly having multiple distinct solutions that are valid to find.) This can make judging the consequences of interventions rather difficult: randomness would also be involved. Overall: To my knowledge no one knows a way to avoid the NP-complete nature of the problem from sometimes having consequences one would otherwise want to avoid, including some uncertainty. Saying that there should be no such problem does not provide any known technique to provide what is requested that does not get back into a NP-complete issue as far as I can tell. Thus, my emphasis on potential improvements in the message, improvements that are tied to the limited information available in the software for the NP-compete problem. It also may be that a man page needs to present information and a reference to such be in the messages produced at run time. It is not a simple context. Note: If bapt reports differently for anything, he has far more context than I do. Without explicit evidence otherwise, believe bapt generally, not me.
(In reply to Mark Millard from comment #7) Better wording and categorising, I agree. But if this is (purely) informational, why have this printed at this 'normal' output level? Why not move this kind of output to some 'verbose' type or even 'debug-level' type output?