[Bug 286740] ports-mgmt/pkg: 2.1.2 Cannot solve problem using SAT solver, trying another plan

https://bugs.freebsd.org/bugzilla/show_bug.cgi?id=286740

Mark Millard <marklmi26-fbsd@yahoo.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |marklmi26-fbsd@yahoo.com

--- Comment #5 from Mark Millard <marklmi26-fbsd@yahoo.com> ---
(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 .

-- 
You are receiving this mail because:
You are the assignee for the bug.