Caption and more info below table.

Each cell has two pieces of data:

* Time in seconds:

- In the case of packup, we also show the size of the sorting networks: the number of wires and the number of comparators. In the case of dynamic sorting networks, we show the size of the largest sorting networks.

* one of the following letters:

- t (if the solver reached a timeout (180 seconds); the numbers that follow are the values of the objective functions for the feasible solution output by the solver

- u (if the solver outputs UNSAT)

- w (if the output is wrong)

- s (if the output is a feasible solution and is suboptimal; the numbers that follow are the objective values)

- b (if the output is a solution and no better solution was found; the numbers that follow are the objective values)

142 Benchmarks: From the Mancoosi International Solver Competition 2011. Available here.

All solutions and objective values were checked using the Mancoosi cudf solution checker available here.

Environment: 24 core Intel(R) Xeon(R) E5-2630 v2 CPU 2.60GHz machines with Debian Linux operating system.

* All solvers and tools were run with a single thread.

Algorithms and Solvers:

* The package upgradeability tool mccs , version 1.1, implements the ILP-based algorithm, explained in this report. The algorithm is adapted from this work in the context of Constraint Programming. mccs was run with the following ILP solvers:

- Gurobi, version 9.0.3

- CPLEX, version 12.10.0

- SCIP, version 7.0.1

- Cbc, version devel, build date: January 14 2021

- GLPK, version v4.65

- lpsolve, version 5.5.2.5

* The package upgradeability tool packup was linked to a C++ library implementing SAT-based leximax optimisation algorithms. The following algorithms were tested:

Non-core-guided algorithms (static sorting networks, each with the largest possible size):

- linear-su (Linear SAT-UNSAT search)

- linear-us (Linear UNSAT-SAT search)

- binary (Binary search)

Core-guided algorithms:

- core-static (Static sorting networks)

- core-merge (Dynamic sorting networks that grow by sorting the new variables and merging with the old sorting networks)

- core-rebuild (Dynamic sorting networks that grow by rebuilding the sorting networks and deleting the old encoding - does not allow continuous incremental SAT solving)

- core-rebuild-incr (Dynamic sorting networks that grow by rebuilding the sorting networks; does not delete the old encoding - allows incremental SAT solving)

- core-merge-dc (core-merge + disjoint cores step)

- core-rebuild-dc (core-rebuild + disjoint cores step)

- core-rebuild-incr-dc (core-rebuild-incr + disjoint cores step)

The CaDiCaL incremental SAT solving library was used, version 1.3.1.

Date of experiment: Feb-15-2022