Pseudo-Boolean Competition 2026

Main points to have in mind:

• Globally, the PB26 competition will be organized as PB25, but there are a few minor changes.
• A steering committee (Carlos Ansótegui, Johannes Fichte, Jakob Nordström, Olivier Roussel) is in charge of defining the rules of the competition, before the actual competition starts.
• This year, the main rankings will be based on PAR-2 scoring (Penalized Average Runtime). An unsolved instance counts as 2 times the time limit, and solvers are ranked on their average run time. The lexicographic ranking used in previous editions will be kept as a secondary ranking. In this latter ranking, solvers are ranked on the number of definitive answers (UNSAT, SAT in the DEC category, OPT in the OPT category) they give in each category. Ties are broken on the cumulated CPU/wall-clock time to give these answers.
• Four tracks will be opened unconditionnaly: PBS (PB Satisfaction) and PBO (PB Optimization) for linear constraints, with and without certificate of unsatisfiability/optimality. Certificates of unsatisfiability/optimality must be generated in the VeriPB format. These tracks are opened to both sequential and parallel solvers.
• Other tracks (WBO, non-linear contraints) will be opened if there is sufficient interest (enough solvers, enough instances).
• As in previous competitions, coefficients in PB constraints can contain an arbitrary number of digits. Solvers are expected to use at least 64 bit integers but they are not required to use arbitrary precision integers. When an instance contains integers that are too large for the solver, it must detect this at parse time and report a 's UNSUPPORTED' answer. This will be used to identify instances supported by all solvers and generate a separate ranking on these. The keyword "intsize" on the first line in the competition format gives information on the size of integers required to handle an instance.
• Solvers may print diagnostic lines (optionally). These lines follow the pattern "d VARIABLE VALUE". They are used to collect some relevant information, such as the number of conflicts for a CDCL solvers (e.g. "d CONFLICTS 8465873"). These diagnostics will be collected and available after the competition for further analysis.
• No contestant may submit more than 3 solvers per track, which means one may appear as an author of at most 3 solvers in a given track. This limit is meant to keep the CPU cost of the competition acceptable.
• A short conformance test will be run before the competition starts. Its goal is to identify early possible problems with solvers in the competition environment but it is not meant to debug or check the correctness of solvers. It is expected that solvers are fully tested by their authors before the competition. It is important to emphasize that solvers must flush the output each time they print an 'o ' line (otherwise the timestamps will be incorrect).
• The resources allocated to solvers should be the same as for PB25: 1 h CPU time and 31 GB RAM per job for a sequential solver, a 100 GB limit for the size of OPT/UNSAT proofs and a 5 h limit for the verification by VeriPB. Parallel solvers should be run on at least 8 cores, with a 1 h wall clock time limit. These limits may be adjusted if required. The hardware used is likely to be the same as last year (see the PB24 slides for details), but this is not guaranteed.
• Anyone may submit new instances to the competition, but the number of selected new instances for a given submitter may not exceed 5% of the final benchmarks selection in a track.
• This year, the number of easy instances included in the selection will be limited. The exact limit and the definition of easy will be detailed later, as well as the selection process.
• Benchmarks submitters will be asked to classify their instances.
• Since it is often hard to collect information on the solvers and benchmarks after the end of the competition, we'll ask submitters to provide information at submission time.

• Solvers generating UNSAT/OPT proofs may optionally use the unchecked deletion mode of VeriPB. A specific option will be added in the submission form soon. Here are the details.

  Since VeriPB proof logging is not only used for unsatisfiability proofs but also to certify satisfiability and optimality, some extra care is needed to deal with deletions of constraints in the input formula and more generally of constraints in the so-called core set of constraints.

  By default VeriPB operates in checked deletion mode, i.e., deletions from the core set have to be justified by deriving the constraint from the remaining core set by an explicit subproof or autoproving. When VeriPB encounters a deletion from the core that can not be autoproven https://gitlab.com/MIAOresearch/software/VeriPB#autoproving and for which no subproof is presented, VeriPB will switch to so-called unchecked deletion mode. What this means in more technical detail is that deletions of constraints from the core set do not need to be justified if no order is loaded or the derived set is empty. However, since unchecked deletions can introduce spurious solutions, any claims about solutions need to be substantiated at the end of the proof.

  In general, proof generation and checking can be made (much) faster in unchecked deletion mode, and therefore the checked deletion mode can be disabled directly by passing the command line option |--no-checkDeletion| to the VeriPB proof checker. In this case, the final conclusion section https://gitlab.com/MIAOresearch/software/VeriPB#conclusion-section of the proof should specify a solution for any claims about solutions in conclusion BOUNDS or conclusion SAT to be verifiable. The solution specified as a hint for the conclusion must be an assignment that satisfies the original formula. In addition, for an optimization problem this solution should yield an objective function value equal to the claimed upper bound.

  If checked deletion mode is used, then there is no need to specify a solution for conclusion BOUNDS or conclusion SAT. Instead, it is sufficient to justify the upper bound by logging solutions using sol or soli in the proof proper. Also, with checked deletion it is not necessary to empty the set of derived constraints in order to be able to delete from the core set while an order is loaded.

Pure portfolios (meta-solvers that do not actually try to satisfy PB contraints but merely call other PB solvers) will be ranked separetely. Authors will have to indicate which solvers are used in such portfolios.

When a solver provides even one single wrong answer in a given category of benchmarks, the solver's results in that category cannot be trusted. Therefore, such a solver will not appear in the final ranking, but its results will still be published on the competition web site. Authors will be allowed to submit a fixed version of their solver (with a maximum of 3 fixed versions).
In the PBS track (decision problem), wrong answers consists in answering SAT and giving a model that does not satisfy all contraints, or answering UNSAT when another solvers has found a model. In the PBO track (optimization problem), wrong answers consists in answering SAT or OPT and giving a model that does not satisfy all constraints, or answering OPT while another solver has found a better solution, or answering UNSAT when another solver has found a model.
In the certified OPT/UNSAT tracks, in addition to the previous cases, a solver that answers OPT or UNSAT and generates a proof that is identified as invalid by VeriPB will be considered incorrect and not ranked. However, even in this case, this solver will not be disqualified in the PBS/PBO tracks (unless another solver finds a model!). When VeriPB cannot validate a proof within its time or memory limit, the corresponding instance is simply counted as OPT/UNSAT instead of certified OPT/UNSAT in the certified track.
In the WBO tracks, a solver is incorrect if it answers UNSAT while another solver found a correct solution, or if it answers SAT or OPT but the provided model violates a hard constraint or its cost is greater or equal to the top cost, or if the solver answers OPT but another solver has found a correct solution with a smaller cost.