Encoding Cardinality Constraints using Multiway Merge Selection Networks - experimental evaluation

by Michał Karpiński and Marek Piotrów

Here we present detailed results of the experiments section of our paper called Encoding Cardinality Constraints using Multiway Merge Selection Networks, that will appear in the proceedings of the 24th International Conference on Principles and Practice of Constraint Programming (CP 2018). In the paper we present a novel encoding based on selection network: 4-Odd-Even Selection Network.

Encodings:

We use the following encodings/solvers in the evaluation:

• 4OE: 4-Odd-Even Selection Networks
• PCN: Pairwise Cardinality Networks (our implementation)
• CA: Binary Adders (from MiniSat+)
• CB: Binary Decision Diagrams (from MiniSat+)
• CS: Odd-Even Sorting Networks (from MiniSat+)
• PBLib: pbSolver from the PBLib ver. 1.2.1, by Tobias Philipp and Peter Steinke
• NPS: npSolver by Norbert Manthey and Peter Steinke

Details about PCN can be found in this paper: link. The newest implementation of MiniSat+ can be found here. Our implementation of 4OE and PCN can be found here. All experiments were carried out on the machines with Intel(R) Core(TM) i7-2600 CPU @ 3.40GHz. Description of benchmarks and the results now follows.

Benchmarks:

A set of benchmarks from the Pseudo-Boolean Evaluation 2015 is used. One of the categories of the competition was DEC-LIN-32-CARD, which contains 2289 instances -- we use these in our evaluation. Every instance is a set of cardinality constraints. This set of benchmarks were evaluated using COMiniSatPS.

Results: results-final.ods.

Cactus plot: