Integrating SMT solver into Portage

[Hexorg]

Hello all, it's that time of the year again - another post about wanting to improve portage. I actually did it... Sort of.

I'm currently failing 179/259 unit tests, but for installing generic packages - it works and is ~2x faster than the native method.

I'm going to have to expand the search space to allow portage to reason about uninstalling the packages, so that 2x can go down, but the good news is that actual solving is nearly instantaneous (~0.004s) What takes a long time is to build the actual SMT equation - I need to iterate over all of the installed packages and add different DEPEND/RDEPEND variables.

I've reached out to #gentoo-portage on IRC and someone there suggested I write a blog post about my dealings with the beast so here it is

I'm all ears about your thoughts on my methodology. It's a lot less trivial than I anticipated.

[b11n]

that's a really good write-up, thanks for sharing it

[szatox]

Wow, that's a good piece, well done!

Complete search: Z3 explores the entire solution space mathematically
Proof generation: Z3 can explain why no solution exists (UNSAT cores)

This looks great, and I suppose that searching for the best solution could reduce impact of merge history on current state, and also opens the door to improving on

Minimal relaxation: Find smallest set of changes needed

The smallest set of changes can mean different things to different people, but it seems this could actually offer several options to choose from.