use a SAT solver to calculate dependencies

[stefantalpalaru]

Details: https://research.swtch.com/version-sat

Importance:

root# time emerge -uDUpv @world

These are the packages that would be merged, in order:

Calculating dependencies... done!
[ebuild     U  ] app-office/gnucash-2.7.7::gentoo [2.7.5::gentoo] USE="nls ofx python sqlite -aqbanking -chipcard -debug -examples -gnome-keyring -mysql -postgres -quotes -register2" PYTHON_TARGETS="python2_7" 0 KiB

Total: 1 package (1 upgrade), Size of downloads: 0 KiB

real    3m4.850s
user    3m0.116s
sys 0m1.506s

(and this is an overclocked FX-8320E@4.4GHz, not some ARM SoC)

[mgorny]

You don't expect me to write one overnight, do you? That said, I don't think writing one is in my current power. I'll probably focus on optimizing the current solver by removing more complex hacks and focusing on providing good input rather than working around the bad input developers give.

[mgorny]

(and 3 minutes is actually quite a good result for Portage)

[stefantalpalaru]

Would you be open to a contribution using an external C++ library like https://www.msoos.org/cryptominisat4/ ?

[mgorny]

Generally I don't mind extra deps but in this case it'd strongly depend on someone actually doing the integration. There are two requirements though:

1. It should be optional / have Python fallback (e.g. to existing solver), so that people can still use Portage without building it first or when it goes boom due to gcc upgrade.
2. License must be reasonably compatible. If it's GPL, that's best but any OSS license should work as long as the Portage integration remains GPL.

[stefantalpalaru]

The license is fine - mostly MIT - https://github.com/msoos/cryptominisat/blob/master/LICENSE.txt

Yes, an opt-in solver behind a new USE flag and "emerge" argument was what I had in mind.

[jansegre]

libsolv seems good too. It may be a good start to just have an interface for using an external solver, so different implementations can be tested and compared.

[mgorny]

Yes, if someone is working on this, I'd suggest focusing on having a one-of-N switch, rather than binary y/n between two resolvers. But I won't be expecting miracles ;-).

I presume you know all the problems with SAT from the recent mailing list threads?

[stefantalpalaru]

I presume you know all the problems with SAT from the recent mailing list threads?

We do now: https://archives.gentoo.org/gentoo-dev/message/40f9585ba6a9850eb82853d945d608eb

[joakim-tjernlund]

libsolv would be great, especially if it could be used by qmerge in portage-utils(qmerge is binary pkg merger written in C)