XCSP 2019 Solvers Competition: benchmark selection (draft)

This year, the selection of instances will be automated. This document describes the selection procedure.

Generalities

Hardness estimation

The hardness of an instance can be defined as the minimum time required to solve it (by any solver that has no prior knowledge of that instance). In practice, this hardness will be estimated by running a limited number of solvers.

The hardness of an instances (hardness score) will be evaluated by averaging the PAR2 score of the top 3 solvers of the last competition, with a timeout set to 40 minutes. Only one version of a solver may appear in this top 3. In 2018, the top 3 solvers in the CSP main track were scop (order+MapleCOMSPS), PicatSAT (2018-08-14) and Mistral-2.0 (2018-08-01). In the COP main track, the top 3 solvers were PicatSAT (2018-08-14), Concrete (3.9.2) and Choco-solver (4.0.7b seq (e747e1e)).

Using only 3 solvers for estimating the hardness introduces a slight but obvious bias. Using the VBS would be slightly better, but is not computationally affordable. As an illustration, it takes 698 days of CPU time to evaluate the hardness of 24451 instances with 3 solvers.

The PAR2 score is equal to the CPU time of the solver when the instance is solved, and 2 times the timeout when the instance is unsolved (when the solver reaches the timeout, or doesn't answer for any other reason). In CSP, the instance is solved when the solver answers SAT or UNSAT. In COP, the instance is solved when the solver answers OPT or UNSAT.

Instances selection (theory)

Here are the rules governing the instances selection:

Instances selection (practice)

In practice, it was sometimes impossible to satisfy all rules (because the list of instances was not diverse enough) and some rules were slightly simplified to facilitate the implementation. Here are the changes that have been made to stay as close as possible to the above rules, while avoiding unsatisfiable constraints.

Publication

The program and data used to perform the selection is available in the archive XCSP19-selection.tar.gz. The SHA512 hash of the program and data files was sent to contestants (to guarantee that the organizers can't change the selection) but the selection was not disclosed until the end of the competition (to prevent any possibility to tune one's solver).