\myheading{Version 3: \ac{MUS}: get info about conflicts}

In case of conflict, my toy package manager just gives "UNSAT", which is probably not a very useful response.
Can we get more information, which packages conflicts?

I use PicoMUS utility here.

The PicoMUS utility from picosat SAT solver suite will tell, which CNF clauses are to be removed to make UNSAT instance SAT.
But for that we need to track, which clauses may be related to which packages.

For example, when IMPLY constraints are added, they clause numbers (from \verb|c.CNF_next_idx|) are saved into a dictionary:

\begin{lstlisting}[style=custompy]
    for p in range(0, packages_total):
        for v in deps[p].keys():
            tmp=[s.OR_list(version_range_to_list_of_vars(dep[0], dep[1], dep[2])) for dep in deps[p][v]]
            if len(tmp)>0:
                if get_MUS:
                    clause_start=s.CNF_next_idx+1
                s.IMPLY_always(vars[p][v], s.AND_list(tmp))
                if get_MUS:
                    clause_stop=s.CNF_next_idx-1+1
                    #print ("IMPLY", p, v, "clauses=[", clause_start, clause_stop, "]")
                    [IMPLY_clauses_packages[c].add(p) for c in range(clause_start, clause_stop+1)]
\end{lstlisting}

And when PicoMUS utility returns list of clauses, we get a list of packages from our records, that are connected to these clauses:

\begin{lstlisting}[style=custompy]
        print ("running picomus")
        MUS_clauses, MUS_vars=s.get_MUS_vars()
...
        IMPLY_clauses_packages_out=set()
...
        for c in MUS_clauses:
...
            if c in IMPLY_clauses_packages.keys():
                IMPLY_clauses_packages_out.update(IMPLY_clauses_packages[c])
...
        print ("conflicted packages (IMPLY):", sorted(list(IMPLY_clauses_packages_out)))
\end{lstlisting}

We also keep tabs on clauses added when fixing packages user wants to install and clauses generated during conflict.json file
processing.

Now a small example.

\begin{lstlisting}[caption=vers.json]
{
        "0" : [2011, 2016],
        "1" : [2013, 2018],
        "2" : [2010, 2015]
}
\end{lstlisting}

\begin{lstlisting}[caption=deps.json]
{
"0":
{
    "2011" : [],
    "2016" : []
},
"1":
{
    "2013" : [],
    "2018" : []
},
"2":
{
    "2010" : [],
    "2015" : []
}
}
\end{lstlisting}

\begin{lstlisting}[caption=conflicts.json]
[
[[1, 2013, 2018], [2, 2010, 2015]]
]
\end{lstlisting}

And I'm trying to 'install' packages 0, 1 and 2, which is impossible:

\begin{lstlisting}
% python3 v3.py test2 0 1 2
get_first_solution, get_MUS= False
initial_pkgs: [0, 1, 2]
going to run solver
UNSAT
get_first_solution, get_MUS= True
initial_pkgs: [0, 1, 2]
running picomus
conflicted packages (set by user): [1, 2]
conflicted packages (IMPLY): []
conflicted packages (from conflicts.json): [1, 2]
\end{lstlisting}

Now you see that packages 1 and 2 cannot be installed with each other.

Another example (test6). Package 1 requires package 0 of version 2014 (only this version)
and package 2 requires package 0 version 2011 only:

\begin{lstlisting}
{
"0":
{
    "2011" : [],
    "2014" : []
},
"1":
{
    "2018" : [[0,2014,2014]]
},
"2":
{
    "2015" : [[0,2011,2011]]
}
}
\end{lstlisting}

My toy package manager find the conflict:

\begin{lstlisting}
% python3 v3.py test6 1 2
get_first_solution, get_MUS= False
initial_pkgs: [1, 2]
going to run solver
UNSAT
get_first_solution, get_MUS= True
initial_pkgs: [1, 2]
running picomus
conflicted packages (set by user): [1, 2]
conflicted packages (IMPLY): [1, 2]
conflicted packages (from conflicts.json): []
\end{lstlisting}

Now example from my randomly generated test data (test100):

\begin{lstlisting}
% python3 v3.py test200 138
get_first_solution, get_MUS= False
initial_pkgs: [138]
going to run solver
UNSAT
get_first_solution, get_MUS= True
initial_pkgs: [138]
running picomus
conflicted packages (set by user): [138]
conflicted packages (IMPLY): [1, 2, 3, 4, 5, 6, 8, 9, 11, 12, 13, 14, 15, 16, 21, 22, 28, 30, 31, 32, 34, 35, 37, 40, 44, 45, 50, 51, 54, 56, 58, 59, 61, 63, 70, 78, 81, 83, 85, 97, 98, 126, 128, 137, 138]
conflicted packages (from conflicts.json): [12, 30, 52, 61]
\end{lstlisting}

Unfortunately, PicoMUS is slow and usable only for debugging.
It may take minutes to find a \ac{MUS}.

On my Intel Core 2 Duo CPU clocked at 2.13GHz:

\begin{lstlisting}
python3 v3.py test200 187  102.24s user 0.15s system 99% cpu 1:43.05 total
python3 v3.py test500 492  101.44s user 0.17s system 99% cpu 1:41.92 total
python3 v3.py test1000 980  38.11s user 0.17s system 99% cpu 38.602 total
\end{lstlisting}

It's unlikely, an end user would wait this long.
But my tests are much more complex than real-world cases, such as Ubuntu packages, etc.
So it can be usable.

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