Pseudo-Boolean Competition 2025

List of slight changes in the rules since the first publication:

• 2025-04-03: The paragraph describing what happens when a solver gives a wrong answer has been rephrased for clarification
• 2025-04-19: 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.

Main points to have in mind:

• Globally, the PB25 competition will be organized as PB24.
• 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.
• Last year, a warm up phase was organized before the actual competition. This year, the warn up phase will be replaced by a shorter conformance test. While the goal is still to identify early possible problems with solvers, the time spent will be much shorter (only one or two days after the final deadline) and we expect solvers to be fully tested by their authors before the competition. Submitting a solver to this conformance test before the final deadline (early May) is welcome (but only a limited number of times !).
• As last year, 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.
• A new track will try to identify how well solver scale on parametric benchmarks as the size/difficulty of the instance increases. As an example, solvers will be tested on the well known Pigeon Hole Problem as well as other combinatorial problems. Participation to this track will be automatic for solvers submitted in other tracks. Since this track is an experimentation, all the details are not defined yet and there might be no official ranking in the end.
• 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.
• As last year, 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. If needed, constestants may be asked to set priorities on their solvers, in order to be sure their most valuable solvers will be run before the SAT conference. In the unlikely case where all experiments cannot be completed before the SAT conference, the remaining experiments will be completed after the conference.
• The resources allocated to solvers should be the same as for PB24: 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 should be the same as last year (see the PB24 slides for details).
• 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.
• Benchmarks selection will be done as last year, with a random selection of a fixed number of instances per family (see this page for details).

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.