\myheading{Version 2: maximize versions}

The package manager in this form is somewhat useless --- an end-user would want to get newest version for each package.
So we would maximize them.

This problem seems to be natural to be solved using MaxSAT solver, and I tried, but stuck with a problem:
MaxSAT solver tries to raise all package's versions, including 'invisible' ones, not limiting to the ones
that has been picked during solving.

This is the algorithm I've conceived:

\begin{lstlisting}
Get an initial solution (like in version 1);

Pick a package/version from solution, fix it at highest version, check
if SAT:
    Leave it as is, pick another package/version
if UNSAT:
    Decrement current version until SAT
\end{lstlisting}

Example trace:

\begin{lstlisting}
% python3 v2.py test100 5
get_first_solution
initial_pkgs: [5]
going to run solver
SAT
first solution:
0:2018; 5:2006;
trying version 2015 for package 5
SAT
solution: 0:2018; 1:2020; 4:2020; 5:2015;
trying version 2020 for package 4
fixed_versions: {5: 2015}
SAT
solution: 0:2018; 1:2020; 4:2020; 5:2015;
trying version 2020 for package 1
fixed_versions: {5: 2015, 4: 2020}
SAT
solution: 0:2018; 1:2020; 4:2020; 5:2015;
trying version 2018 for package 0
fixed_versions: {5: 2015, 4: 2020, 1: 2020}
SAT
solution: 0:2018; 1:2020; 4:2020; 5:2015;
final solution: 0:2018; 1:2020; 4:2020; 5:2015;
\end{lstlisting}

Now here I'm trying to 'install' package 4 and 11.
My toy package manager tries to raise versions of all packages, including dependent ones:

\begin{lstlisting}
% python3 v2.py test100 4 11
get_first_solution
initial_pkgs: [4, 11]
going to run solver
SAT
first solution:
4:2020; 11:2007;
trying version 2018 for package 11
SAT
solution: 0:2018; 1:2006; 4:2020; 5:2015; 11:2018;
trying version 2015 for package 5
fixed_versions: {11: 2018}
SAT
solution: 0:2018; 1:2006; 4:2020; 5:2015; 11:2018;
trying version 2020 for package 4
fixed_versions: {11: 2018, 5: 2015}
SAT
solution: 0:2018; 1:2006; 4:2020; 5:2015; 11:2018;
trying version 2020 for package 1
fixed_versions: {11: 2018, 5: 2015, 4: 2020}
SAT
solution: 0:2018; 1:2020; 4:2020; 5:2015; 11:2018;
trying version 2018 for package 0
fixed_versions: {11: 2018, 5: 2015, 4: 2020, 1: 2020}
SAT
solution: 0:2018; 1:2020; 4:2020; 5:2015; 11:2018;
final solution: 0:2018; 1:2020; 4:2020; 5:2015; 11:2018;
\end{lstlisting}

By the way, it's important to note that the first solution can coincide with the 'best' solution.
But may not.

\lstinputlisting[style=custompy,caption=The source code]{\CURPATH/files/v2.py}