Benchmarks selection
Random selection in the general case
Overall, the selection of benchmarks is done randomly, selecting (when possible) the same number of instances per domain. A domain is a set of similar instances. Basically, one directory in an archive equals one domain, but some directories must be merged into a single domain when they contain similar instances. At most 5% of the whole instance set can be selected per submitter. This is meant to avoid anyone to have too much influence on the competition results.The classification obtained in 2024 was kept (thanks again to Johannes Fichte). New instances submitted to PB25 or PB26 were classified by the organizer according to the name of the directories.
The goal was to obtain between 300 and 600 instances in the DEC-LIN and OPT-LIN tracks. Given the number of domains, 10 instances were randomly selected per domain in all tracks, except in the DEC-LIN track where 15 instances per domain were selected. If a domain doesn't contain enough instances, they are all selected (except when easy instances are taken into account, see below). Duplicate instances are removed. This test is performed by checking the md5 checksum of instances. This means that the check is purely syntactical. It doesn't identify that an instance where contraints are reordered or variables renamed can be the same as another instance.
The 5% limit per submitter was not hit.
Easy instances
This year, the steering committee decided to limit the number of "easy" instances in the main tracks of the competition (DEC-LIN, OPT-LIN) because many instances were solved in a very short amount of time during PB25. Giving a definition of "easy" is not so easy. In fact, an instance (and more generally a problem) is easy for an algorithm (in other words a solver or a class of solvers). The most sensible definition of easy would be solvable by at least one algorithm within low complexity bounds. But that definition is purely theoretical and it doesn't make sense in a competition, where the goal is to limit the number of instances that every team can solve. We have to switch to a practical, experimental definition. Of course, we can hardly afford to run every solver on every instance. Therefore, we have to select a short subset of representative solvers. After some iterations and experiments, it was decided to consider as easy an instance that could be solved within 60 seconds by each solver in the representative set of solvers. That set was obtained by selecting the 3 best contributors to the VBS (Virtual Best Solver) as well as the two last generic solvers in the ranking of the last competition. Picking the 3 best contributors allows to approximate the VBS with a short list of solvers (3).Picking the 2 last generic solvers in the last competition ranking allows to avoid a too strong bias towards the best solvers. Of course, that definition is not perfect, but it makes sense.
The best contributor to the VBS is the solver that solves the largest number of instances. The second best contributor is the solver that solves the largest number of instances that remained unsolved by the best solver. Similarly, the third best contirbutor is the solver the largest number of instances that remained unsolved by the two previously selected solvers.
In the DEC-LIN track, the 3 best contributors are: SCIP-NaPS 1.00a2 with 406 solved instances, LSIPExact S1 with a marginal contribution of 34 instances and Sat4j CP 2025-06-06 with a marginal contribution of 9 instances. The two last generic solvers in the DEC-LIN track are SCIP 2025-06-13 and Sat4j CP 2025-06-06. Interestingly, Sat4j CP is both the third contirbutor to the VBS and the last generic solver.
In the OPT-LIN track, the 3 best contributors are UWrMaxSat-SCIP 2025-06-04 with 358 solved instances, ExactPR-S 2025-06-01 with a marginal contribution of 29 instances and OR-Tools CP-SAT 9.14 with a marginal contribution of 16 instances. The two last generic solvers in the OPT-LIN track are Sat4j CP 2025-06-06 and toulbar2 2025-06-13
In the end, with the above definitions, over all the instances submitted to the compeition up to 2025, there are 7430 easy instances out of 20906 in the DEC-LIN track (35,5 %), and 2352 easy instances out of 15268 in the OPT-LIN track (15.4 %)
The steering committee considered a limit on the number of easy instances between 10% and 20% of the selection. There was no unanimity, but in the end a limit of 20% was chosen for this year. This means that this limit is already satisfied in the OPT-LIN track, and a pure random selection was used as last year, with 10 instances per domain of benchmarks. In the DEC-LIN track, we must move from 35% of easy instances to 20%. Since the goal is to select 15 instances per domain in that track (as last year), we should pick 3 easy instances and 12 harder instances in each domain. Of course, we don't have enough easy/harder instances in each domain. So the idea is to select enough harder instances in the domains where they are available. The number of easy/harder instances to select in each domain could have been computed automatically (for example with constraints) but the selection process would have become more complex and harder to reproduce. Therefore, per domain limits were enforced manually based on the number of available instances (with the target of 3 easy, 12 harder) and luckily the global selection didn't exceed the 20% limit so no other manual adjustment was needed. The selection program accepts a new directive "N easy E", which means select randomly N instances with at most E easy instances in the domain. The list of easy instances is stored in two files: easy-dec.list and easy-opt.list.
It was also planned to select one instance every other k instances in series that are parameterized and that are build to have a complexity increasing with the value of the parameter. However, the list of those series could not be identified in time for the competition and this selection method couldn't be applied.
Benchmarks submitted this year were not evaluated to identify easy instances, and a pure random selection was done.
Actual selection
The archive PB26-selection.tgz (updated) contains the source files used to perform the selection. The program was run on a system with glibc 2.40-26 (Fedora 41). The random seed used is 2026. The archive contains:
- runSelection: this is the script that runs the selection process in all categories. Running this script will generate *-selection.list files (as well as *-selection.sql files, which are used for registering the selection in the database). The *-selection.list files contain the list of selected instances.
- {dec-lin,dec-nlc,opt-lin,opt-nlc,wbo}.list: these are the list of available instances, grouped by domains, with the number of instances to select per domain
- md5.list: fingerprint of each intance
- select.cc: the program performing the random selection. It is derived from the one available on https://www.cril.univ-artois.fr/XCSP19/selection/. It adds support for removal of duplicates (based on the md5 fingerprint). This program was written in a rush and therefore is not well documented, not efficient and doesn't forgive any mistake in the input.
- savedSelection/: contains the selection actually used for the competition. Running the selection script should yield the same files as in this directory.
Selecting instances is a difficult subject. The selection made is not perfect and some mistakes were probably made. However, it is hopefully clear that the selection was automated, mainly random and largely independent of the submitted solvers.
Hardware used
The competition was run on the CRIL cluster. We used new hardware this year: 10 nodes with two AMD EPYC 9355 processors, 3,55GHz, 32 cores (64 hyperthreads), 256 MB cache, DDR5-6400, 1TiB RAM. The same nodes were used for sequential solvers and parallel solvers.
Resources limits
Of course, the goal is to run as many solvers as possible at the same time, but we need to limit the interferences between the solvers running on the same host. For best reproducibility, a single solver should be run on one host, but this requires way too much resources. For the most efficient use of resources, each core could be used to run one solver, but that slows down the solvers. An acceptable balance must be found. In this competition, it's been considered that a slowdown of 10% is acceptable. The number of jobs that could be run concurrently to respect this limit was determined experimentally with a subset of solvers submitted to PB24 (Exact, naps, picat, roudingsat, Sat4j, SCIP).
On a node, from 1 to 64 instances of the same solver on the same instance were run. The number of concurrent execution of a solver is denoted by jobsPerNode and takes a value in {1, 2, 4, 8, 16,32, 64}. The file average-E.csv reports the results of 3 different tests, where the time of each execution for a given configuration (value of jobsPerNode) is reported as well as the average, minimum and maximum time. The ratio of the average CPU time for the given value of jobsPerNode over the average CPU time for jobsPerNode=1 is also given. It can be observed that this ratio remains very close to 1 for jobsPerNode=16, but exceeds 1.1 (+10%) for nbJobsPerNode=32 in several cases. Therefore, it was decided to run 16 instances of a given sequential solver at the same time on a node.
The figures show graphically the results of the CSV file. Vertical lines are drawn for jobsPerNode=1, 2, 4, 8, 16,32 and 64. They represent the number of concurrent executions of a solver on a node. Just after the vertical line, jobsPerNode points represent the time mesured for each of these executions. It can be observed that Sat4j (written in Java) has a very strange behaviour, with a very significant dispersion of the runtimes, and more surprisingly a runtime that decreases for jobPerNodes=64. This was already observed on the hardware used for PB24 and PB25, and remains unexplained. For the other solvers, the runtimes remain quite stable from one run to another, but as expected, increase with jobsPerNode.
At any time, only one solver is running on a host, but most often several different instances of the same solver are run concurrently. It means that if a job is running solver X, all other jobs on the host run the same solver X. This guarantees that a solver cannot interfere with another competitor's solver.
- Sequential solvers were allowed to use at most 1 h of CPU time and at most 3700 s of wall clock time. They were allowed to use 62000 MiB of memory. Sixteen instances of the same solver were run simultaneously on a host.
- Parallel solvers were allowed to use at most 16 h of CPU time and at most 3700 s of wall clock time. They were allowed to use 248000 MiB of memory. Four instances of the same solver were run simultaneously on a host.
- veripb+cakepb was run with a 5 h CPU time limit (with a maximum of 18300 s of wall clock time) and a 62000 MiB memory limit. The output of VeriPB was sent directly to CakePB through a pipe (actually a FIFO, a.k.a. named pipe). The two processes were running simultaneously.
UNSAT/OPT proofs and I/O limits
Solvers in the CERT tracks can generate proofs that are as large as 100 GiB (a limit set for the competition and enforced by runsolver). They can generate proofs at approximately 50 MB/s. With 16 executions of a solver in parallel, 1.6 TB of proofs could be generated at the same time on a node, at a rate of 500 MB/s. With ten nodes running concurrently, we can reach 16 TB generated at a rate of 5 GB/s.
It was soon discovered during the warm-up that the I/O limits of our cluster were exceeded. In fact, several hosts mostly crashed and the wall-clock time of the jobs was significantly greater than the CPU time, because the processes were waiting in the D state (disk I/O). The problem was even worse since in the warm-up, 32 jobs per node were run (since the runtime doesn't really matter) and since the /tmp was too small, every proof file was written to a NFS server.
It should be mentioned that this problem didn't occur in the previous competitions because only 4 jobs were running on a host and proofs were written to /tmp, which was large enough.
A first step was to extend the size of the /tmp partition as much as possible, to reach 700 GB. This is already quite large, but insufficient to store 1.6 TB of proofs at a time.
To solve the problem, a specific caching filesystem was written to compress proofs on the fly. It took several iterations to get it right. Solvers write files to this filesystem. Blocks of data are first stored in a cache in RAM. 12 threads compress the blocks stored in the cache and write them to their final destination. Those threads take the place of 3 jobs, which means we can only run 13 instances of a solver in the CERT track at a time, implying a slowdown of the experiments of 25 %. The size of the RAM cache is 186 GB. If necessary, the cache is extended by using a temporary file on /tmp, with a limit of 700 GB. In the final configuration of the filesystem, with the fastest compression level of gzip, the 12 threads were sufficient to compress in real time the proofs. But in previous versions, with a higher and hence slower compression level, the RAM cache kept filling, and became eventually full. When this occurs, the write call is suspended, waiting for some room to become available in the cache. The solver si suspended in a D state, as for a real disk, and since we only take into account the CPU time, this has no influence on the results.
Happy end of the story? Not exactly. A late submission is using different threads in a portfolio setup, and generates one proof per thread. At the end, only one of the proofs is kept (the one generated by the thread that answers). This means that the I/O problem probably still remains with this kind of solver. However, that solver was not run with 16 cores and the problem hasn't occurred in this edition of the competition.
It should be noticed that more than 5 TB of compressed proofs were generated during the competition. Out of them, only 700 GB are useful. Proofs are useless for answers other than UNSAT and OPT and can be removed immediately.