\myheading{Version 1: just get a solution}

\leveldown{}

I'm assigning a boolean variable to each package/version.

\myheading{Making only one version per package possible}

First, only one version per package is allowed, so I'm using one-hot encoding and 'AtMost1' constraint for each package.
However, a bit may be absent at all. It will leave version value in undefined state.

\myheading{IMPLY constraint}

Second, for each dependency, I'm adding an IMPLY constraint.
If a package 1 version 2004 requires package 2 versions 2000..2002, the following constraint is to be added:

\begin{lstlisting}
pkg-1-ver-2004 => pkg-2-ver-2000 OR pkg-2-ver-2001 OR pkg-2-ver-2002
\end{lstlisting}

($\implies$ is a sign for logical implication.)

That means that if pkg-1-ver-2004=True, one of pkg-2-... must be also true.
However, converse is not required.
It's possible that pkg-2-ver-2002=True, but pkg-1-ver-2004=False.

See the wikipedia page about it\footnote{\url{https://en.wikipedia.org/wiki/Material_conditional}}.

For a common computer programmer, this can be explained in terms of algol-like programming language:

\begin{lstlisting}
if pkg-1-ver-2004:
    set True to one of these: pkg-2-ver-2000 OR pkg-2-ver-2001 OR pkg-2-ver-2002
if another package/version:
    set True to ...
\end{lstlisting}

... but these things wouldn't work in reverse.

\myheading{Handling conflicts}

For example, package 1 versions [2000..2001] cannot be installed simultaneously with package 2 versions [2005..2007].
I'll add this constraint:

\begin{lstlisting}
AND(pkg-1-ver-2000 OR pkg-1-ver-2001, pkg-2-ver-2005 OR pkg-2-ver-2006 OR pkg-2-ver-2007)=False
\end{lstlisting}

...or...

\begin{lstlisting}
NOT(AND(pkg-1-ver-2000 OR pkg-1-ver-2001, pkg-2-ver-2005 OR pkg-2-ver-2006 OR pkg-2-ver-2007))==True
\end{lstlisting}

NAND gate can also be called "not both".
In my example, in plain English language,
that means:
"pkg-1-ver-2000 OR pkg-1-ver-2001 cannot be true if pkg-2-ver-2005 OR pkg-2-ver-2006 OR pkg-2-ver-2007 is also true and vice versa".

In other words, these two OR expressions cannot be both true, but can be both false.

\myheading{Getting solution}

You'll get a correct solution, but other package/versions may also be turned on.
Because you can't 'ground' them to false by default.
'Unconnected packages' are 'dangling' chaotically each time you run SAT solver.

My idea is to collect information from solution recursively, starting at the initial list of desired packages supplied by an end-user.
See the \verb|collect_from_solution_recursively()| function.

\myheading{Test}

Let's take a test data from 'test100' folder and run it:

\begin{lstlisting}
% python3 v1.py test100 0 1 5 10 50
get_first_solution
initial_pkgs: [0, 1, 5, 10, 50]
going to run solver
SAT
first solution:
0:2018; 1:2020; 2:2019; 3:2019; 4:2020; 5:2015; 6:2016; 7:2020; 8:2014; 10:2015; 11:2018; 12:2019; 13:2020; 14:2012; 15:2020; 16:2017; 17:2019; 18:2020; 19:2018; 21:2020; 22:2000; 23:2001; 28:2001; 29:2020; 34:2020; 35:2014; 36:2015; 50:2014;
\end{lstlisting}

The solution is correct, but versions are 'random' (in allowed limits), not maximized.

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

\levelup{}